Analysis I, Section 11.2: Piecewise constant functions

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Piecewise constant functions.
• The piecewise constant integral.

@[reducible, inline]

abbrev Chapter11.Constant {X Y : Type} (f : X → Y) : Prop

Definition 11.2.1

Equations

• Chapter11.Constant f = ∃ (c : Y), ∀ (x : X), f x = c

@[reducible, inline]

noncomputable abbrev Chapter11.constant_value {X Y : Type} [hY : Nonempty Y] (f : X → Y) : Y

Equations

• Chapter11.constant_value f = if h : Chapter11.Constant f then Exists.choose h else hY.some

theorem Chapter11.Constant.eq {X Y : Type} {f : X → Y} [Nonempty Y] (h : Constant f) (x : X) : f x = constant_value f

theorem Chapter11.Constant.of_const {X Y : Type} {f : X → Y} {c : Y} (h : ∀ (x : X), f x = c) : Constant f

theorem Chapter11.Constant.const_eq {X Y : Type} {f : X → Y} [hX : Nonempty X] [Nonempty Y] {c : Y} (h : ∀ (x : X), f x = c) : constant_value f = c

theorem Chapter11.Constant.of_subsingleton {X Y : Type} [hs : Subsingleton X] [hY : Nonempty Y] {f : X → Y} : Constant f

@[reducible, inline]

abbrev Chapter11.ConstantOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Equations

• Chapter11.ConstantOn f X = Chapter11.Constant fun (x : ↑X) => f ↑x

@[reducible, inline]

noncomputable abbrev Chapter11.constant_value_on (f : ℝ → ℝ) (X : Set ℝ) : ℝ

Equations

• Chapter11.constant_value_on f X = Chapter11.constant_value fun (x : ↑X) => f ↑x

theorem Chapter11.ConstantOn.eq {f : ℝ → ℝ} {X : Set ℝ} (h : ConstantOn f X) {x : ℝ} (hx : x ∈ X) : f x = constant_value_on f X

theorem Chapter11.ConstantOn.of_const {f : ℝ → ℝ} {X : Set ℝ} {c : ℝ} (h : ∀ x ∈ X, f x = c) : ConstantOn f X

theorem Chapter11.ConstantOn.of_const' (c : ℝ) (X : Set ℝ) : ConstantOn (fun (x : ℝ) => c) X

theorem Chapter11.ConstantOn.const_eq {f : ℝ → ℝ} {X : Set ℝ} (hX : X.Nonempty) {c : ℝ} (h : ∀ x ∈ X, f x = c) : constant_value_on f X = c

theorem Chapter11.ConstantOn.congr {f g : ℝ → ℝ} {X : Set ℝ} (h : ∀ x ∈ X, f x = g x) : ConstantOn f X ↔ ConstantOn g X

theorem Chapter11.ConstantOn.congr' {f g : ℝ → ℝ} {X : Set ℝ} (hf : ConstantOn f X) (h : ∀ x ∈ X, f x = g x) : ConstantOn g X

theorem Chapter11.ConstantOn.of_subsingleton {f : ℝ → ℝ} {X : Set ℝ} [Subsingleton ↑X] : ConstantOn f X

theorem Chapter11.constant_value_on_congr {f g : ℝ → ℝ} {X : Set ℝ} (h : ∀ x ∈ X, f x = g x) : constant_value_on f X = constant_value_on g X

@[reducible, inline]

abbrev Chapter11.PiecewiseConstantWith (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) : Prop

Definition 11.2.3 (Piecewise constant functions I)

Equations

• Chapter11.PiecewiseConstantWith f P = ∀ J ∈ P, Chapter11.ConstantOn f ↑J

theorem Chapter11.PiecewiseConstantWith.def (f : ℝ → ℝ) {I : BoundedInterval} {P : Partition I} : PiecewiseConstantWith f P ↔ ∀ J ∈ P, ∃ (c : ℝ), ∀ x ∈ J, f x = c

theorem Chapter11.PiecewiseConstantWith.congr {f g : ℝ → ℝ} {I : BoundedInterval} {P : Partition I} (h : ∀ x ∈ ↑I, f x = g x) : PiecewiseConstantWith f P ↔ PiecewiseConstantWith g P

@[reducible, inline]

abbrev Chapter11.PiecewiseConstantOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

Definition 11.2.5 (Piecewise constant functions I)

Equations

• Chapter11.PiecewiseConstantOn f I = ∃ (P : Chapter11.Partition I), Chapter11.PiecewiseConstantWith f P

theorem Chapter11.PiecewiseConstantOn.def (f : ℝ → ℝ) (I : BoundedInterval) : PiecewiseConstantOn f I ↔ ∃ (P : Partition I), ∀ J ∈ P, ConstantOn f ↑J

theorem Chapter11.PiecewiseConstantOn.congr {f g : ℝ → ℝ} {I : BoundedInterval} (h : ∀ x ∈ ↑I, f x = g x) : PiecewiseConstantOn f I ↔ PiecewiseConstantOn g I

theorem Chapter11.PiecewiseConstantOn.congr' {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (h : ∀ x ∈ ↑I, f x = g x) : PiecewiseConstantOn g I

@[reducible, inline]

noncomputable abbrev Chapter11.f_11_2_4 : ℝ → ℝ

Example 11.2.4 / Example 11.2.6

Equations

• Chapter11.f_11_2_4 x = if x < 1 then 0 else if x < 3 then 7 else if x = 3 then 4 else if x < 6 then 5 else if x = 6 then 2 else 0

theorem Chapter11.ConstantOn.piecewiseConstantOn {f : ℝ → ℝ} {I : BoundedInterval} (h : ConstantOn f ↑I) : PiecewiseConstantOn f I

Example 11.2.6

theorem Chapter11.PiecewiseConstantWith.mono {f : ℝ → ℝ} {I : BoundedInterval} {P P' : Partition I} (hPP' : P ≤ P') (hP : PiecewiseConstantWith f P) : PiecewiseConstantWith f P'

Lemma 11.2.7 / Exercise 11.2.1

theorem Chapter11.PiecewiseConstantOn.add {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn (f + g) I

Lemma 11.2.8 / Exercise 11.2.2

theorem Chapter11.PiecewiseConstantOn.sub {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn (f - g) I

Lemma 11.2.8 / Exercise 11.2.2

theorem Chapter11.PiecewiseConstantOn.max {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn (f ⊔ g) I

Lemma 11.2.8 / Exercise 11.2.2

theorem Chapter11.PiecewiseConstantOn.min {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn (f ⊓ g) I

Lemma 11.2.8 / Exercise 11.2.2

theorem Chapter11.PiecewiseConstantOn.mul {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : PiecewiseConstantOn (f * g) I

Lemma 11.2.8 / Exercise 11.2.2

theorem Chapter11.PiecewiseConstantOn.smul {f : ℝ → ℝ} {I : BoundedInterval} (c : ℝ) (hf : PiecewiseConstantOn f I) : PiecewiseConstantOn (c • f) I

Lemma 11.2.8 / Exercise 11.2.2

theorem Chapter11.PiecewiseConstantOn.div {f g : ℝ → ℝ} {I : BoundedInterval} (hf hg : PiecewiseConstantOn f I) : PiecewiseConstantOn (f / g) I

Lemma 11.2.8 / Exercise 11.2.2. I believe the hypothesis that g does not vanish is not needed.

@[reducible, inline]

noncomputable abbrev Chapter11.PiecewiseConstantWith.integ (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) : ℝ

Definition 11.2.9 (Piecewise constant integral I)

Equations

• Chapter11.PiecewiseConstantWith.integ f P = ∑ J ∈ P.intervals, Chapter11.constant_value_on f ↑J * J.length

theorem Chapter11.PiecewiseConstantWith.integ_congr {f g : ℝ → ℝ} {I : BoundedInterval} {P : Partition I} (h : ∀ x ∈ ↑I, f x = g x) : integ f P = integ g P

@[reducible, inline]

noncomputable abbrev Chapter11.f_11_2_12 : ℝ → ℝ

Example 11.2.12

Equations

• Chapter11.f_11_2_12 x = if x < 3 then 2 else if x = 3 then 4 else 6

@[reducible, inline]

noncomputable abbrev Chapter11.P_11_2_12 : Partition (BoundedInterval.Icc 1 4)

Equations

• Chapter11.P_11_2_12 = (⊥.join ⊥ Chapter11.P_11_2_12._proof_1).join ⊥ Chapter11.P_11_2_12._proof_2

@[reducible, inline]

noncomputable abbrev Chapter11.P_11_2_12' : Partition (BoundedInterval.Icc 1 4)

Equations

• Chapter11.P_11_2_12' = (((⊥.join ⊥ Chapter11.P_11_2_12'._proof_1).join ⊥ Chapter11.P_11_2_12._proof_1).join ⊥ Chapter11.P_11_2_12._proof_2).add_empty

theorem Chapter11.PiecewiseConstantWith.integ_eq {f : ℝ → ℝ} {I : BoundedInterval} {P P' : Partition I} (hP : PiecewiseConstantWith f P) (hP' : PiecewiseConstantWith f P') : integ f P = integ f P'

Proposition 11.2.13 (Piecewise constant integral is independent of partition) / Exercise 11.2.3

@[reducible, inline]

noncomputable abbrev Chapter11.PiecewiseConstantOn.integ (f : ℝ → ℝ) (I : BoundedInterval) : ℝ

Definition 11.2.14 (Piecewise constant integral II)

Equations

• Chapter11.PiecewiseConstantOn.integ f I = if h : Chapter11.PiecewiseConstantOn f I then Chapter11.PiecewiseConstantWith.integ f (Exists.choose h) else 0

@[reducible, inline]

noncomputable abbrev Chapter11.PiecewiseConstantOn.integ' {f : ℝ → ℝ} {I : BoundedInterval} : PiecewiseConstantOn f I → ℝ

Equations

• x✝.integ' = Chapter11.PiecewiseConstantOn.integ f I

theorem Chapter11.PiecewiseConstantOn.integ_def {f : ℝ → ℝ} {I : BoundedInterval} {P : Partition I} (h : PiecewiseConstantWith f P) : integ f I = PiecewiseConstantWith.integ f P

theorem Chapter11.PiecewiseConstantOn.integ_congr {f g : ℝ → ℝ} {I : BoundedInterval} (h : ∀ x ∈ ↑I, f x = g x) : integ f I = integ g I

theorem Chapter11.PiecewiseConstantOn.integ_add {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : integ (f + g) I = integ f I + integ g I

Theorem 11.2.16 (a) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_smul {f : ℝ → ℝ} {I : BoundedInterval} (c : ℝ) (hf : PiecewiseConstantOn f I) : integ (c • f) I = c * integ f I

Theorem 11.2.16 (b) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_sub {f g : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : integ (f - g) I = integ f I - integ g I

Theorem 11.2.16 (c) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_of_nonneg {f : ℝ → ℝ} {I : BoundedInterval} (h : ∀ x ∈ I, 0 ≤ f x) (hf : PiecewiseConstantOn f I) : 0 ≤ integ f I

Theorem 11.2.16 (d) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_mono {f g : ℝ → ℝ} {I : BoundedInterval} (h : ∀ x ∈ I, f x ≤ g x) (hf : PiecewiseConstantOn f I) (hg : PiecewiseConstantOn g I) : integ f I ≤ integ g I

Theorem 11.2.16 (e) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_const (c : ℝ) (I : BoundedInterval) : integ (fun (x : ℝ) => c) I = c * I.length

Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_const' {f : ℝ → ℝ} {I : BoundedInterval} (h : ConstantOn f ↑I) : integ f I = constant_value_on f ↑I * I.length

Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.of_extend {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : PiecewiseConstantOn f I) : PiecewiseConstantOn (fun (x : ℝ) => if x ∈ I then f x else 0) J

Theorem 11.2.16 (g) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_of_extend {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : PiecewiseConstantOn f I) : integ (fun (x : ℝ) => if x ∈ I then f x else 0) J = integ f I

Theorem 11.2.16 (g) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.of_join {I J K : BoundedInterval} (hIJK : K.joins I J) (f : ℝ → ℝ) : PiecewiseConstantOn f K ↔ PiecewiseConstantOn f I ∧ PiecewiseConstantOn f J

Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4

theorem Chapter11.PiecewiseConstantOn.integ_of_join {I J K : BoundedInterval} (hIJK : K.joins I J) {f : ℝ → ℝ} (h : PiecewiseConstantOn f K) : integ f K = integ f I + integ f J

Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4