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.
namespace Chapter11open BoundedInterval
open Classical in
noncomputable abbrev constant_value {X Y:Type} [hY: Nonempty Y] (f:X → Y) : Y :=
if h: Constant f then h.choose else hY.sometheorem Constant.eq {X Y:Type} {f: X → Y} [Nonempty Y] (h: Constant f) (x:X) :
f x = constant_value f := X:TypeY:Typef:X → Yinst✝:Nonempty Yh:Constant fx:X⊢ f x = constant_value f X:TypeY:Typef:X → Yinst✝:Nonempty Yh:Constant fx:X⊢ f x = Exists.choose ⋯; All goals completed! 🐙theorem Constant.of_const {X Y:Type} {f:X → Y} {c:Y} (h: ∀ x, f x = c) :
Constant f := X:TypeY:Typef:X → Yc:Yh:∀ (x : X), f x = c⊢ Constant f All goals completed! 🐙theorem Constant.const_eq {X Y:Type} {f:X → Y} [hX: Nonempty X] [Nonempty Y] {c:Y} (h: ∀ x, f x = c) :
constant_value f = c := X:TypeY:Typef:X → YhX:Nonempty Xinst✝:Nonempty Yc:Yh:∀ (x : X), f x = c⊢ constant_value f = c All goals completed! 🐙theorem Constant.of_subsingleton {X Y:Type} [hs: Subsingleton X] [hY: Nonempty Y] {f:X → Y} :
Constant f := X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Y⊢ Constant f
X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty X⊢ Constant fX:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:¬Nonempty X⊢ Constant f
X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty X⊢ Constant f X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty X⊢ ∀ (x : X), f x = f h.some; X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty Xx✝:X⊢ f x✝ = f h.some; X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:Nonempty Xx✝:X⊢ x✝ = h.some; All goals completed! 🐙
X:TypeY:Typehs:Subsingleton XhY:Nonempty Yf:X → Yh:IsEmpty X⊢ Constant f; All goals completed! 🐙abbrev ConstantOn (f: ℝ → ℝ) (X: Set ℝ) : Prop := Constant (fun x : X ↦ f ↑x)noncomputable abbrev constant_value_on (f:ℝ → ℝ) (X: Set ℝ) : ℝ := constant_value (fun x : X ↦ f ↑x)theorem ConstantOn.eq {f: ℝ → ℝ} {X: Set ℝ} (h: ConstantOn f X) {x:ℝ} (hx: x ∈ X) :
f x = constant_value_on f X := f:ℝ → ℝX:Set ℝh:ConstantOn f Xx:ℝhx:x ∈ X⊢ f x = constant_value_on f X
All goals completed! 🐙theorem ConstantOn.of_const {f:ℝ → ℝ} {X: Set ℝ} {c:ℝ} (h: ∀ x ∈ X, f x = c) :
ConstantOn f X := ⟨ c, f:ℝ → ℝX:Set ℝc:ℝh:∀ x ∈ X, f x = c⊢ ∀ (x : ↑X), (fun x => f ↑x) x = c All goals completed! 🐙 ⟩theorem ConstantOn.of_const' (c:ℝ) (X:Set ℝ): ConstantOn (fun _ ↦ c) X := of_const (c := c) (c:ℝX:Set ℝ⊢ ∀ x ∈ X, c = c All goals completed! 🐙)theorem ConstantOn.const_eq {f:ℝ → ℝ} {X: Set ℝ} (hX: X.Nonempty) {c:ℝ} (h: ∀ x ∈ X, f x = c) :
constant_value_on f X = c := f:ℝ → ℝX:Set ℝhX:X.Nonemptyc:ℝh:∀ x ∈ X, f x = c⊢ constant_value_on f X = c
All goals completed! 🐙theorem ConstantOn.congr {f g: ℝ → ℝ} {X: Set ℝ} (h: ∀ x ∈ X, f x = g x) : ConstantOn f X ↔ ConstantOn g X := f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ ConstantOn f X ↔ ConstantOn g X
f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (Constant fun x => f ↑x) = Constant fun x => g ↑x; f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (fun x => f ↑x) = fun x => g ↑x; All goals completed! 🐙theorem ConstantOn.congr' {f g: ℝ → ℝ} {X: Set ℝ} (hf: ConstantOn f X) (h: ∀ x ∈ X, f x = g x) : ConstantOn g X := (congr h).mp hftheorem ConstantOn.of_subsingleton {f: ℝ → ℝ} {X: Set ℝ} [Subsingleton X] :
ConstantOn f X := Constant.of_subsingletontheorem 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 := f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ constant_value_on f X = constant_value_on g X
f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (constant_value fun x => f ↑x) = constant_value fun x => g ↑x; f:ℝ → ℝg:ℝ → ℝX:Set ℝh:∀ x ∈ X, f x = g x⊢ (fun x => f ↑x) = fun x => g ↑x; All goals completed! 🐙Definition 11.2.3 (Piecewise constant functions I)
abbrev PiecewiseConstantWith (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) : Prop := ∀ J ∈ P, ConstantOn f (J:Set ℝ)theorem PiecewiseConstantWith.def (f:ℝ → ℝ) {I: BoundedInterval} {P: Partition I} :
PiecewiseConstantWith f P ↔ ∀ J ∈ P, ∃ c, ∀ x ∈ J, f x = c := f:ℝ → ℝI:BoundedIntervalP:Partition I⊢ PiecewiseConstantWith f P ↔ ∀ J ∈ P, ∃ c, ∀ x ∈ J, f x = c
All goals completed! 🐙theorem PiecewiseConstantWith.congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
(h: ∀ x ∈ (I:Set ℝ), f x = g x) :
PiecewiseConstantWith f P ↔ PiecewiseConstantWith g P := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ PiecewiseConstantWith f P ↔ PiecewiseConstantWith g P
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ (∀ J ∈ P, ConstantOn f ↑J) ↔ ∀ J ∈ P, ConstantOn g ↑J; f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P⊢ ConstantOn f ↑J ↔ ConstantOn g ↑J
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P⊢ ∀ x ∈ ↑J, f x = g x; f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ Pthis:?_mvar.35023 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ x ∈ ↑J, f x = g x; All goals completed! 🐙Definition 11.2.5 (Piecewise constant functions I)
abbrev PiecewiseConstantOn (f:ℝ → ℝ) (I: BoundedInterval) : Prop := ∃ P : Partition I, PiecewiseConstantWith f Ptheorem PiecewiseConstantOn.def (f:ℝ → ℝ) (I: BoundedInterval):
PiecewiseConstantOn f I ↔ ∃ P : Partition I, ∀ J ∈ P, ConstantOn f (J:Set ℝ) := f:ℝ → ℝI:BoundedInterval⊢ PiecewiseConstantOn f I ↔ ∃ P, ∀ J ∈ P, ConstantOn f ↑J All goals completed! 🐙theorem PiecewiseConstantOn.congr {f g: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), f x = g x) :
PiecewiseConstantOn f I ↔ PiecewiseConstantOn g I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g x⊢ PiecewiseConstantOn f I ↔ PiecewiseConstantOn g I
All goals completed! 🐙theorem PiecewiseConstantOn.congr' {f g: ℝ → ℝ} {I: BoundedInterval} (hf: PiecewiseConstantOn f I) (h: ∀ x ∈ (I:Set ℝ), f x = g x) : PiecewiseConstantOn g I := (congr h).mp hfExample 11.2.4 / Example 11.2.6
noncomputable abbrev f_11_2_4 : ℝ → ℝ := fun x ↦
if x < 1 then 0 else -- junk value
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 -- junk valueexample : PiecewiseConstantOn f_11_2_4 (Icc 1 6) := ⊢ PiecewiseConstantOn f_11_2_4 (Icc 1 6)
⊢ PiecewiseConstantWith f_11_2_4
{ intervals := {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6}, exists_unique := ?w.refine_1, contains := ?w.refine_2 }⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6} ∧ x ∈ J⊢ ∀ J ∈ {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6}, J ⊆ Icc 1 6
⊢ PiecewiseConstantWith f_11_2_4
{ intervals := {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6}, exists_unique := ?w.refine_1, contains := ?w.refine_2 } All goals completed! 🐙
⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 3, Icc 3 3, Ioo 3 6, Icc 6 6} ∧ x ∈ J All goals completed! 🐙
All goals completed! 🐙example : PiecewiseConstantOn f_11_2_4 (Icc 1 6) := ⊢ PiecewiseConstantOn f_11_2_4 (Icc 1 6)
⊢ PiecewiseConstantWith f_11_2_4
{ intervals := {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6}, exists_unique := ?w.refine_1,
contains := ?w.refine_2 }⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6} ∧ x ∈ J⊢ ∀ J ∈ {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6}, J ⊆ Icc 1 6
⊢ PiecewiseConstantWith f_11_2_4
{ intervals := {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6}, exists_unique := ?w.refine_1,
contains := ?w.refine_2 } All goals completed! 🐙
⊢ ∀ x ∈ Icc 1 6, ∃! J, J ∈ {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 3, Ioo 3 5, Ico 5 6, Icc 6 6} ∧ x ∈ J All goals completed! 🐙
All goals completed! 🐙Example 11.2.6
theorem ConstantOn.piecewiseConstantOn {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f (I:Set ℝ)) :
PiecewiseConstantOn f I := f:ℝ → ℝI:BoundedIntervalh:ConstantOn f ↑I⊢ PiecewiseConstantOn f I All goals completed! 🐙Lemma 11.2.7 / Exercise 11.2.1
theorem PiecewiseConstantWith.mono {f:ℝ → ℝ} {I: BoundedInterval} {P P': Partition I} (hPP': P ≤ P')
(hP: PiecewiseConstantWith f P) : PiecewiseConstantWith f P' := f:ℝ → ℝI:BoundedIntervalP:Partition IP':Partition IhPP':P ≤ P'hP:PiecewiseConstantWith f P⊢ PiecewiseConstantWith f P'
All goals completed! 🐙Lemma 11.2.8 / Exercise 11.2.2
theorem PiecewiseConstantOn.add {f g: ℝ → ℝ} {I: BoundedInterval}
(hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (f + g) I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f + g) I
All goals completed! 🐙Lemma 11.2.8 / Exercise 11.2.2
theorem PiecewiseConstantOn.sub {f g: ℝ → ℝ} {I: BoundedInterval}
(hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (f - g) I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f - g) I
All goals completed! 🐙Lemma 11.2.8 / Exercise 11.2.2
theorem PiecewiseConstantOn.max {f g: ℝ → ℝ} {I: BoundedInterval}
(hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (max f g) I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f ⊔ g) I
All goals completed! 🐙Lemma 11.2.8 / Exercise 11.2.2
theorem PiecewiseConstantOn.min {f g: ℝ → ℝ} {I: BoundedInterval}
(hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (min f g) I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f ⊓ g) I
All goals completed! 🐙Lemma 11.2.8 / Exercise 11.2.2
theorem PiecewiseConstantOn.mul {f g: ℝ → ℝ} {I: BoundedInterval}
(hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) : PiecewiseConstantOn (f * g) I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantOn (f * g) I
All goals completed! 🐙Lemma 11.2.8 / Exercise 11.2.2
theorem PiecewiseConstantOn.smul {f: ℝ → ℝ} {I: BoundedInterval}
(c:ℝ) (hf: PiecewiseConstantOn f I) : PiecewiseConstantOn (c • f) I := f:ℝ → ℝI:BoundedIntervalc:ℝhf:PiecewiseConstantOn f I⊢ PiecewiseConstantOn (c • f) I
All goals completed! 🐙
Lemma 11.2.8 / Exercise 11.2.2. I believe the hypothesis that g does not vanish is not needed.
theorem PiecewiseConstantOn.div {f g: ℝ → ℝ} {I: BoundedInterval}
(hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn f I) : PiecewiseConstantOn (f / g) I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn f I⊢ PiecewiseConstantOn (f / g) I
All goals completed! 🐙Definition 11.2.9 (Piecewise constant integral I)
noncomputable abbrev PiecewiseConstantWith.integ (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) :
ℝ := ∑ J ∈ P.intervals, constant_value_on f (J:Set ℝ) * |J|ₗtheorem PiecewiseConstantWith.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
(h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f P = integ g P := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ integ f P = integ g P
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g x⊢ ∀ x ∈ P.intervals, constant_value_on f ↑x * x.length = constant_value_on g ↑x * x.length; f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * J.length = constant_value_on g ↑J * J.length; f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J = constant_value_on g ↑J; f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervals⊢ ∀ x ∈ ↑J, f x = g x
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ih:∀ x ∈ ↑I, f x = g xJ:BoundedIntervalhJ:J ∈ P.intervalsthis:?_mvar.39776 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ x ∈ ↑J, f x = g x; All goals completed! 🐙Example 11.2.12
noncomputable abbrev f_11_2_12 : ℝ → ℝ := fun x ↦
if x < 3 then 2 else
if x = 3 then 4 else
6noncomputable abbrev P_11_2_12 : Partition (Icc 1 4) :=
((⊥: Partition (Ico 1 3)).join (⊥ : Partition (Icc 3 3))
(join_Ico_Icc (⊢ 1 ≤ 3 All goals completed! 🐙) (⊢ 3 ≤ 3 All goals completed! 🐙) )).join
(⊥: Partition (Ioc 3 4))
(join_Icc_Ioc (⊢ 1 ≤ 3 All goals completed! 🐙) (⊢ 3 ≤ 4 All goals completed! 🐙))example : PiecewiseConstantWith f_11_2_12 P_11_2_12 := ⊢ PiecewiseConstantWith f_11_2_12 P_11_2_12
All goals completed! 🐙example : PiecewiseConstantWith.integ f_11_2_12 P_11_2_12 = 10 := ⊢ PiecewiseConstantWith.integ f_11_2_12 P_11_2_12 = 10
All goals completed! 🐙noncomputable abbrev P_11_2_12' : Partition (Icc 1 4) :=
((((⊥: Partition (Ico 1 2)).join (⊥ : Partition (Ico 2 3))
(join_Ico_Ico (⊢ 1 ≤ 2 All goals completed! 🐙) (⊢ 2 ≤ 3 All goals completed! 🐙) )).join
(⊥: Partition (Icc 3 3))
(join_Ico_Icc (⊢ 1 ≤ 3 All goals completed! 🐙) (⊢ 3 ≤ 3 All goals completed! 🐙))).join
(⊥: Partition (Ioc 3 4))
(join_Icc_Ioc (⊢ 1 ≤ 3 All goals completed! 🐙) (⊢ 3 ≤ 4 All goals completed! 🐙))).add_emptyexample : PiecewiseConstantWith f_11_2_12 P_11_2_12' := ⊢ PiecewiseConstantWith f_11_2_12 P_11_2_12'
All goals completed! 🐙example : PiecewiseConstantWith.integ f_11_2_12 P_11_2_12' = 10 := ⊢ PiecewiseConstantWith.integ f_11_2_12 P_11_2_12' = 10
All goals completed! 🐙Proposition 11.2.13 (Piecewise constant integral is independent of partition) / Exercise 11.2.3
theorem PiecewiseConstantWith.integ_eq {f:ℝ → ℝ} {I: BoundedInterval} {P P': Partition I}
(hP: PiecewiseConstantWith f P) (hP': PiecewiseConstantWith f P') : integ f P = integ f P' := f:ℝ → ℝI:BoundedIntervalP:Partition IP':Partition IhP:PiecewiseConstantWith f PhP':PiecewiseConstantWith f P'⊢ integ f P = integ f P'
All goals completed! 🐙open Classical in
/-- Definition 11.2.14 (Piecewise constant integral II) -/
noncomputable abbrev PiecewiseConstantOn.integ (f:ℝ → ℝ) (I: BoundedInterval) :
ℝ := if h: PiecewiseConstantOn f I then PiecewiseConstantWith.integ f h.choose else 0noncomputable abbrev PiecewiseConstantOn.integ' {f:ℝ → ℝ} {I: BoundedInterval} (_:PiecewiseConstantOn f I) := integ f Itheorem PiecewiseConstantOn.integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
(h: PiecewiseConstantWith f P) : integ f I = PiecewiseConstantWith.integ f P := f:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f P⊢ integ f I = PiecewiseConstantWith.integ f P
have h' : PiecewiseConstantOn f I := f:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f P⊢ integ f I = PiecewiseConstantWith.integ f P All goals completed! 🐙
f:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f Ph':Chapter11.PiecewiseConstantOn _fvar.43611 _fvar.43612 := ?_mvar.43620⊢ PiecewiseConstantWith.integ f (Exists.choose ⋯) = PiecewiseConstantWith.integ f P; All goals completed! 🐙theorem PiecewiseConstantOn.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval}
(h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f I = integ g I := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g x⊢ integ f I = integ g I
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f I⊢ integ f I = integ g If:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f I⊢ integ f I = integ g I
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f I⊢ integ f I = integ g If:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f I⊢ integ f I = integ g I (f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f Ihg:?_mvar.48511 := _fvar.46959⊢ integ f I = integ g I; f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:¬PiecewiseConstantOn f Ihg:¬PiecewiseConstantOn g I⊢ integ f I = integ g I; All goals completed! 🐙)
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantWith g (Exists.choose ⋯)
f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ ↑I, f x = g xhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ PiecewiseConstantWith f (Exists.choose ⋯); All goals completed! 🐙Example 11.2.15
example : PiecewiseConstantOn.integ f_11_2_4 (Icc 1 6) = 10 := ⊢ PiecewiseConstantOn.integ f_11_2_4 (Icc 1 6) = 10
All goals completed! 🐙Theorem 11.2.16 (a) (Laws of integration) / Exercise 11.2.4
theorem 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 := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ integ (f + g) I = integ f I + integ g I
All goals completed! 🐙Theorem 11.2.16 (b) (Laws of integration) / Exercise 11.2.4
theorem PiecewiseConstantOn.integ_smul {f: ℝ → ℝ} {I: BoundedInterval} (c:ℝ) (hf: PiecewiseConstantOn f I) :
integ (c • f) I = c * integ f I
:= f:ℝ → ℝI:BoundedIntervalc:ℝhf:PiecewiseConstantOn f I⊢ integ (c • f) I = c * integ f I
All goals completed! 🐙Theorem 11.2.16 (c) (Laws of integration) / Exercise 11.2.4
theorem 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 := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ integ (f - g) I = integ f I - integ g I
All goals completed! 🐙Theorem 11.2.16 (d) (Laws of integration) / Exercise 11.2.4
theorem PiecewiseConstantOn.integ_of_nonneg {f: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ I, 0 ≤ f x)
(hf: PiecewiseConstantOn f I) :
0 ≤ integ f I := f:ℝ → ℝI:BoundedIntervalh:∀ x ∈ I, 0 ≤ f xhf:PiecewiseConstantOn f I⊢ 0 ≤ integ f I
All goals completed! 🐙Theorem 11.2.16 (e) (Laws of integration) / Exercise 11.2.4
theorem 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 := f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:∀ x ∈ I, f x ≤ g xhf:PiecewiseConstantOn f Ihg:PiecewiseConstantOn g I⊢ integ f I ≤ integ g I
All goals completed! 🐙Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4
theorem PiecewiseConstantOn.integ_const (c: ℝ) (I: BoundedInterval) :
integ (fun _ ↦ c) I = c * |I|ₗ := c:ℝI:BoundedInterval⊢ integ (fun x => c) I = c * I.length
All goals completed! 🐙Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4
theorem PiecewiseConstantOn.integ_const' {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f I) :
integ f I = (constant_value_on f I) * |I|ₗ := f:ℝ → ℝI:BoundedIntervalh:ConstantOn f ↑I⊢ integ f I = constant_value_on f ↑I * I.length
All goals completed! 🐙open Classical in
/-- Theorem 11.2.16 (g) (Laws of integration) / Exercise 11.2.4 -/
theorem 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 := I:BoundedIntervalJ:BoundedIntervalhIJ:I ⊆ Jf:ℝ → ℝh:PiecewiseConstantOn f I⊢ PiecewiseConstantOn (fun x => if x ∈ I then f x else 0) J
All goals completed! 🐙open Classical in
/-- Theorem 11.2.16 (g) (Laws of integration) / Exercise 11.2.4 -/
theorem 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 := I:BoundedIntervalJ:BoundedIntervalhIJ:I ⊆ Jf:ℝ → ℝh:PiecewiseConstantOn f I⊢ integ (fun x => if x ∈ I then f x else 0) J = integ f I
All goals completed! 🐙Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4
theorem PiecewiseConstantOn.of_join {I J K: BoundedInterval} (hIJK: K.joins I J)
(f: ℝ → ℝ) : PiecewiseConstantOn f K ↔ PiecewiseConstantOn f I ∧ PiecewiseConstantOn f J := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalhIJK:K.joins I Jf:ℝ → ℝ⊢ PiecewiseConstantOn f K ↔ PiecewiseConstantOn f I ∧ PiecewiseConstantOn f J
All goals completed! 🐙Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4
theorem 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 := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalhIJK:K.joins I Jf:ℝ → ℝh:PiecewiseConstantOn f K⊢ integ f K = integ f I + integ f J
All goals completed! 🐙end Chapter11