Analysis I, Section 11.8: The Riemann-Stieltjes integral

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:

• Definition of α-length.

• The piecewise constant Riemann-Stieltjes integral.

• The full Riemann-Stieltjes integral.

Technical notes:

• In Lean it is more convenient to make definitions such as α-length and the Riemann-Stieltjes integral totally defined, thus assigning "junk" values to the cases where the definition is not intended to be applied. For the definition of α-length, the definition is intended to be applied in contexts where left and right limits exist, and the function is extended by constants to the left and right of its intended domain of definition; for instance, if a function Unknown identifier `f`f is defined on Unknown identifier `Icc`Icc 0 1, then it is intended that Unknown identifier `f`sorry = sorry : Propf x = Unknown identifier `f`f 1 for all Unknown identifier `x`sorry ≥ 1 : Propx ≥ 1 and Unknown identifier `f`sorry = sorry : Propf x = Unknown identifier `f`f 0 for all Unknown identifier `x`sorry ≤ 0 : Propx ≤ 0; in particular, at a right endpoint, the value of a function is intended to agree with its right limit, and similarly for the left endpoint, although we do not enforce this in our definition of α-length. (For functions defined on open intervals, the extension is immaterial.)

• The notion of α-length and piecewise constant Riemann-Stieltjes integral is intended for situations where left and right limits exist, such as for monotone functions or continuous functions, though technically they make sense without these hypotheses. The full Riemann-Stieltjes integral is intended for functions that are of bounded variation, though we shall restrict attention to the special case of monotone increasing functions for the most part.

namespace Chapter11open BoundedInterval Chapter9 noncomputable abbrev left_lim (f: ℝ → ℝ) (x₀:ℝ) : ℝ := lim ((nhdsWithin x₀ (.Iio x₀)).map f)theorem right_lim_def {f: ℝ → ℝ} {x₀ L:ℝ} (h: Convergesto (.Ioi x₀) f L x₀) : right_lim f x₀ = L := byf:ℝ → ℝx₀:ℝL:ℝh:Convergesto (Set.Ioi x₀) f L x₀⊢ right_lim f x₀ = L apply lim_eqhf:ℝ → ℝx₀:ℝL:ℝh:Convergesto (Set.Ioi x₀) f L x₀⊢ Filter.map f (nhdsWithin x₀ (Set.Ioi x₀)) ≤ nhds L; rwa [Convergesto.iff, Filter.Tendsto.eq_1]hf:ℝ → ℝx₀:ℝL:ℝh:Filter.map f (nhdsWithin x₀ (Set.Ioi x₀)) ≤ nhds L⊢ Filter.map f (nhdsWithin x₀ (Set.Ioi x₀)) ≤ nhds L at htheorem left_lim_def {f: ℝ → ℝ} {x₀ L:ℝ} (h: Convergesto (.Iio x₀) f L x₀) : left_lim f x₀ = L := byf:ℝ → ℝx₀:ℝL:ℝh:Convergesto (Set.Iio x₀) f L x₀⊢ left_lim f x₀ = L apply lim_eqhf:ℝ → ℝx₀:ℝL:ℝh:Convergesto (Set.Iio x₀) f L x₀⊢ Filter.map f (nhdsWithin x₀ (Set.Iio x₀)) ≤ nhds L; rwa [Convergesto.iff, Filter.Tendsto.eq_1]hf:ℝ → ℝx₀:ℝL:ℝh:Filter.map f (nhdsWithin x₀ (Set.Iio x₀)) ≤ nhds L⊢ Filter.map f (nhdsWithin x₀ (Set.Iio x₀)) ≤ nhds L at hnoncomputable abbrev jump (f: ℝ → ℝ) (x₀:ℝ) : ℝ := right_lim f x₀ - left_lim f x₀ theorem right_lim_of_monotone' {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) : right_lim f x₀ = sInf (f '' .Ioi x₀) := right_lim_def (right_lim_of_monotone x₀ hf) theorem left_lim_of_monotone' {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) : left_lim f x₀ = sSup (f '' .Iio x₀) := left_lim_def (left_lim_of_monotone x₀ hf)theorem jump_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) : 0 ≤ jump f x₀ := byf:ℝ → ℝx₀:ℝhf:Monotone f⊢ 0 ≤ jump f x₀ simp [jump, left_lim_of_monotone' x₀ hf, right_lim_of_monotone' x₀ hf]f:ℝ → ℝx₀:ℝhf:Monotone f⊢ sSup (f '' Set.Iio x₀) ≤ sInf (f '' Set.Ioi x₀) apply csSup_le (byf:ℝ → ℝx₀:ℝhf:Monotone f⊢ (f '' Set.Iio x₀).Nonempty simpAll goals completed! 🐙); intro a haf:ℝ → ℝx₀:ℝhf:Monotone fa:ℝha:a ∈ f '' Set.Iio x₀⊢ a ≤ sInf (f '' Set.Ioi x₀) apply le_csInf (byf:ℝ → ℝx₀:ℝhf:Monotone fa:ℝha:a ∈ f '' Set.Iio x₀⊢ (f '' Set.Ioi x₀).Nonempty simpAll goals completed! 🐙); intro b hbf:ℝ → ℝx₀:ℝhf:Monotone fa:ℝha:a ∈ f '' Set.Iio x₀b:ℝhb:b ∈ f '' Set.Ioi x₀⊢ a ≤ b; simp at ha hbf:ℝ → ℝx₀:ℝhf:Monotone fa:ℝb:ℝha:∃ x < x₀, f x = ahb:∃ x, x₀ < x ∧ f x = b⊢ a ≤ b obtain ⟨ x, hx, rfl ⟩ := haintro.introf:ℝ → ℝx₀:ℝhf:Monotone fb:ℝhb:∃ x, x₀ < x ∧ f x = bx:ℝhx:x < x₀⊢ f x ≤ b; obtain ⟨ y, hy, rfl ⟩ := hbintro.intro.intro.introf:ℝ → ℝx₀:ℝhf:Monotone fx:ℝhx:x < x₀y:ℝhy:x₀ < y⊢ f x ≤ f y apply hfintro.intro.intro.intro.af:ℝ → ℝx₀:ℝhf:Monotone fx:ℝhx:x < x₀y:ℝhy:x₀ < y⊢ x ≤ y; grindAll goals completed! 🐙theorem right_lim_le_left_lim_of_monotone {f:ℝ → ℝ} {a b:ℝ} (hab: a < b) (hf: Monotone f) : right_lim f a ≤ left_lim f b := byf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ right_lim f a ≤ left_lim f b rw [left_lim_of_monotone' b hf, right_lim_of_monotone' a hf]f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ sInf (f '' Set.Ioi a) ≤ sSup (f '' Set.Iio b) calc _ ≤ f ((a+b)/2) := byf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ sInf (f '' Set.Ioi a) ≤ f ((a + b) / 2) apply ConditionallyCompleteLattice.csInf_lea._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.70f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ BddBelow (f '' Set.Ioi a)a._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.73f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ f ((a + b) / 2) ∈ f '' Set.Ioi a .a._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.70f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ BddBelow (f '' Set.Ioi a) rw [bddBelow_def]a._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.70f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ ∃ x, ∀ y ∈ f '' Set.Ioi a, x ≤ y; use f ahf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ ∀ y ∈ f '' Set.Ioi a, f a ≤ y; intro y hyhf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fy:ℝhy:y ∈ f '' Set.Ioi a⊢ f a ≤ y; simp at hyhf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fy:ℝhy:∃ x, a < x ∧ f x = y⊢ f a ≤ y; obtain ⟨ x, hx, rfl ⟩ := hyh.intro.introf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fx:ℝhx:a < x⊢ f a ≤ f x; apply hfh.intro.intro.af:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fx:ℝhx:a < x⊢ a ≤ x; grindAll goals completed! 🐙 simpa._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.73f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ ∃ x, a < x ∧ f x = f ((a + b) / 2); use (a+b)/2hf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ a < (a + b) / 2 ∧ f ((a + b) / 2) = f ((a + b) / 2); simphf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ a < (a + b) / 2; linarithAll goals completed! 🐙 _ ≤ _ := byf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ f ((a + b) / 2) ≤ sSup (f '' Set.Iio b) apply ConditionallyCompleteLattice.le_csSupa._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.31f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ BddAbove (f '' Set.Iio b)a._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.34f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ f ((a + b) / 2) ∈ f '' Set.Iio b .a._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.31f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ BddAbove (f '' Set.Iio b) rw [bddAbove_def]a._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.31f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ ∃ x, ∀ y ∈ f '' Set.Iio b, y ≤ x; use f bhf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ ∀ y ∈ f '' Set.Iio b, y ≤ f b; intro y hyhf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fy:ℝhy:y ∈ f '' Set.Iio b⊢ y ≤ f b; simp at hyhf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fy:ℝhy:∃ x < b, f x = y⊢ y ≤ f b; obtain ⟨ x, hx, rfl ⟩ := hyh.intro.introf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fx:ℝhx:x < b⊢ f x ≤ f b; apply hfh.intro.intro.af:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone fx:ℝhx:x < b⊢ x ≤ b; grindAll goals completed! 🐙 simpa._@.Mathlib.Order.ConditionallyCompleteLattice.Defs._hyg.34f:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ ∃ x < b, f x = f ((a + b) / 2); use (a+b)/2hf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ (a + b) / 2 < b ∧ f ((a + b) / 2) = f ((a + b) / 2); simphf:ℝ → ℝa:ℝb:ℝhab:a < bhf:Monotone f⊢ (a + b) / 2 < b; linarithAll goals completed! 🐙 notation3:max α"["I"]ₗ" => α_length α Itheorem α_length_of_empty (α: ℝ → ℝ) {I: BoundedInterval} (hI: (I:Set ℝ) = ∅) : α[I]ₗ = 0 := match I with | Icc _ _ =>α:ℝ → ℝI:BoundedIntervala✝:ℝb✝:ℝhI:↑(Icc a✝ b✝) = ∅⊢ α[Icc a✝ b✝]ₗ = 0 byα:ℝ → ℝI:BoundedIntervala✝:ℝb✝:ℝhI:↑(Icc a✝ b✝) = ∅⊢ α[Icc a✝ b✝]ₗ = 0 simp [Set.Icc_eq_empty_iff] at *α:ℝ → ℝI:BoundedIntervala✝:ℝb✝:ℝhI:b✝ < a✝⊢ a✝ ≤ b✝ → right_lim α b✝ - left_lim α a✝ = 0; grindAll goals completed! 🐙 | Ico a b =>α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhI:↑(Ico a b) = ∅⊢ α[Ico a b]ₗ = 0 byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhI:↑(Ico a b) = ∅⊢ α[Ico a b]ₗ = 0 simp [Set.Ico_eq_empty_iff] at *α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhI:b ≤ a⊢ a ≤ b → left_lim α b - left_lim α a = 0; grindAll goals completed! 🐙 | Ioc a b =>α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhI:↑(Ioc a b) = ∅⊢ α[Ioc a b]ₗ = 0 byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhI:↑(Ioc a b) = ∅⊢ α[Ioc a b]ₗ = 0 simp [Set.Ioc_eq_empty_iff] at *α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhI:b ≤ a⊢ a ≤ b → right_lim α b - right_lim α a = 0; grindAll goals completed! 🐙 | Ioo _ _ =>α:ℝ → ℝI:BoundedIntervala✝:ℝb✝:ℝhI:↑(Ioo a✝ b✝) = ∅⊢ α[Ioo a✝ b✝]ₗ = 0 byα:ℝ → ℝI:BoundedIntervala✝:ℝb✝:ℝhI:↑(Ioo a✝ b✝) = ∅⊢ α[Ioo a✝ b✝]ₗ = 0 simp [Set.Ioo_eq_empty_iff] at *α:ℝ → ℝI:BoundedIntervala✝:ℝb✝:ℝhI:b✝ ≤ a✝⊢ a✝ < b✝ → left_lim α b✝ - right_lim α a✝ = 0; grindAll goals completed! 🐙@[simp] theorem α_length_of_pt {α: ℝ → ℝ} (a:ℝ) : α[Icc a a]ₗ = jump α a := byα:ℝ → ℝa:ℝ⊢ α[Icc a a]ₗ = jump α a simp [α_length, jump]All goals completed! 🐙theorem α_length_of_cts {α:ℝ → ℝ} {I: BoundedInterval} {a b: ℝ} (haa: a < I.a) (hab: I.a ≤ I.b) (hbb: I.b < b) (hI : I ⊆ Ioo a b) (hα: ContinuousOn α (Ioo a b)) : α[I]ₗ = α I.b - α I.a := byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ α[I]ₗ = α I.b - α I.a have ha_left : left_lim α I.a = α I.a := byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ α[I]ₗ = α I.b - α I.a apply left_lim_of_continuous _ (hα.continuousWithinAt (byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ I.a ∈ ↑(Ioo a b) simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ a < I.a ∧ I.a < b; grindAll goals completed! 🐙)) exact ⟨ I.a - a, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ I.a - a > 0 grindAll goals completed! 🐙, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ Set.Ioc (I.a - (I.a - a)) I.a ⊆ ↑(Ioo a b) intro _α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)a✝:ℝ⊢ a✝ ∈ Set.Ioc (I.a - (I.a - a)) I.a → a✝ ∈ ↑(Ioo a b); simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)a✝:ℝ⊢ a < a✝ → a✝ ≤ I.a → a < a✝ ∧ a✝ < b; grindAll goals completed! 🐙 ⟩ have ha_right : right_lim α I.a = α I.a := byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ α[I]ₗ = α I.b - α I.a apply right_lim_of_continuous _ (hα.continuousWithinAt (byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ I.a ∈ ↑(Ioo a b) simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ a < I.a ∧ I.a < b; grindAll goals completed! 🐙)) exact ⟨ b - I.a, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ b - I.a > 0 grindAll goals completed! 🐙, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ Set.Ico I.a (I.a + (b - I.a)) ⊆ ↑(Ioo a b) intro _α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))a✝:ℝ⊢ a✝ ∈ Set.Ico I.a (I.a + (b - I.a)) → a✝ ∈ ↑(Ioo a b); simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))a✝:ℝ⊢ I.a ≤ a✝ → a✝ < b → a < a✝ ∧ a✝ < b; grindAll goals completed! 🐙 ⟩ have hb_left : left_lim α I.b = α I.b := byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ α[I]ₗ = α I.b - α I.a apply left_lim_of_continuous _ (hα.continuousWithinAt (byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ I.b ∈ ↑(Ioo a b) simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ a < I.b ∧ I.b < b; grindAll goals completed! 🐙)) exact ⟨ I.b - a, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ I.b - a > 0 grindAll goals completed! 🐙, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ Set.Ioc (I.b - (I.b - a)) I.b ⊆ ↑(Ioo a b) intro _α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))a✝:ℝ⊢ a✝ ∈ Set.Ioc (I.b - (I.b - a)) I.b → a✝ ∈ ↑(Ioo a b); simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))a✝:ℝ⊢ a < a✝ → a✝ ≤ I.b → a < a✝ ∧ a✝ < b; grindAll goals completed! 🐙 ⟩ have hb_right : right_lim α I.b = α I.b := byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)⊢ α[I]ₗ = α I.b - α I.a apply right_lim_of_continuous _ (hα.continuousWithinAt (byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))hb_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.b _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_9 _fvar.93518 _fvar.93519, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.b _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.b _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_10 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.b _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_8 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ I.b ∈ ↑(Ioo a b) simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))hb_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.b _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_9 _fvar.93518 _fvar.93519, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.b _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.b _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_10 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.b _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_8 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ a < I.b ∧ I.b < b; grindAll goals completed! 🐙)) exact ⟨ b - I.b, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))hb_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.b _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_9 _fvar.93518 _fvar.93519, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.b _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.b _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_10 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.b _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_8 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ b - I.b > 0 grindAll goals completed! 🐙, byα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))hb_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.b _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_9 _fvar.93518 _fvar.93519, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.b _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.b _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_10 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.b _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_8 _fvar.93518 _fvar.93519 _fvar.93520)))⊢ Set.Ico I.b (I.b + (b - I.b)) ⊆ ↑(Ioo a b) intro _α:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))hb_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.b _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_9 _fvar.93518 _fvar.93519, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.b _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.b _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_10 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.b _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_8 _fvar.93518 _fvar.93519 _fvar.93520)))a✝:ℝ⊢ a✝ ∈ Set.Ico I.b (I.b + (b - I.b)) → a✝ ∈ ↑(Ioo a b); simpα:ℝ → ℝI:BoundedIntervala:ℝb:ℝhaa:a < I.ahab:I.a ≤ I.bhbb:I.b < bhI:I ⊆ Ioo a bhα:ContinuousOn α ↑(Ioo a b)ha_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.a _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_4 _fvar.93518, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.a _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_5 _fvar.93519 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))ha_right:Chapter11.right_lim _fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.a _fvar.93515) := Chapter11.right_lim_of_continuous (Exists.intro (_fvar.93517 - Chapter11.BoundedInterval.a _fvar.93515) ⟨Chapter11.α_length_of_cts._proof_6 _fvar.93519 _fvar.93520, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ico (Chapter11.BoundedInterval.a _fvar.93515) x) (add_sub_cancel (Chapter11.BoundedInterval.a _fvar.93515) _fvar.93517)) Set.mem_Ico._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_7 _fvar.93518)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.a _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_3 _fvar.93518 _fvar.93519 _fvar.93520)))hb_left:Chapter11.left_lim _fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) = @_fvar.93514 (Chapter11.BoundedInterval.b _fvar.93515) := Chapter11.left_lim_of_continuous (Exists.intro (Chapter11.BoundedInterval.b _fvar.93515 - _fvar.93516) ⟨Chapter11.α_length_of_cts._proof_9 _fvar.93518 _fvar.93519, fun ⦃a⦄ => Eq.mpr (id (Eq.trans (implies_congr (Eq.trans (congrArg (fun x => a ∈ Set.Ioc x (Chapter11.BoundedInterval.b _fvar.93515)) (sub_sub_cancel (Chapter11.BoundedInterval.b _fvar.93515) _fvar.93516)) Set.mem_Ioc._simp_1) (Eq.trans (congrArg (fun x => a ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) and_imp._simp_1)) (Chapter11.α_length_of_cts._proof_10 _fvar.93520)⟩) (ContinuousOn.continuousWithinAt _fvar.93522 (Eq.mpr (id (Eq.trans (congrArg (fun x => Chapter11.BoundedInterval.b _fvar.93515 ∈ x) (Chapter11.BoundedInterval.set_Ioo _fvar.93516 _fvar.93517)) Set.mem_Ioo._simp_1)) (Chapter11.α_length_of_cts._proof_8 _fvar.93518 _fvar.93519 _fvar.93520)))a✝:ℝ⊢ I.b ≤ a✝ → a✝ < b → a < a✝ ∧ a✝ < b; grindAll goals completed! 🐙 ⟩ cases I with | Icc _ _ =>Iccα:ℝ → ℝa:ℝb:ℝhα:ContinuousOn α ↑(Ioo a b)a✝:ℝb✝:ℝhaa:a < (Icc a✝ b✝).ahab:(Icc a✝ b✝).a ≤ (Icc a✝ b✝).bhbb:(Icc a✝ b✝).b < bhI:Icc a✝ b✝ ⊆ Ioo a bha_left:left_lim α (Icc a✝ b✝).a = α (Icc a✝ b✝).aha_right:right_lim α (Icc a✝ b✝).a = α (Icc a✝ b✝).ahb_left:left_lim α (Icc a✝ b✝).b = α (Icc a✝ b✝).bhb_right:right_lim α (Icc a✝ b✝).b = α (Icc a✝ b✝).b⊢ α[Icc a✝ b✝]ₗ = α (Icc a✝ b✝).b - α (Icc a✝ b✝).a grindAll goals completed! 🐙 | Ico _ _ =>Icoα:ℝ → ℝa:ℝb:ℝhα:ContinuousOn α ↑(Ioo a b)a✝:ℝb✝:ℝhaa:a < (Ico a✝ b✝).ahab:(Ico a✝ b✝).a ≤ (Ico a✝ b✝).bhbb:(Ico a✝ b✝).b < bhI:Ico a✝ b✝ ⊆ Ioo a bha_left:left_lim α (Ico a✝ b✝).a = α (Ico a✝ b✝).aha_right:right_lim α (Ico a✝ b✝).a = α (Ico a✝ b✝).ahb_left:left_lim α (Ico a✝ b✝).b = α (Ico a✝ b✝).bhb_right:right_lim α (Ico a✝ b✝).b = α (Ico a✝ b✝).b⊢ α[Ico a✝ b✝]ₗ = α (Ico a✝ b✝).b - α (Ico a✝ b✝).a grindAll goals completed! 🐙 | Ioc _ _ =>Iocα:ℝ → ℝa:ℝb:ℝhα:ContinuousOn α ↑(Ioo a b)a✝:ℝb✝:ℝhaa:a < (Ioc a✝ b✝).ahab:(Ioc a✝ b✝).a ≤ (Ioc a✝ b✝).bhbb:(Ioc a✝ b✝).b < bhI:Ioc a✝ b✝ ⊆ Ioo a bha_left:left_lim α (Ioc a✝ b✝).a = α (Ioc a✝ b✝).aha_right:right_lim α (Ioc a✝ b✝).a = α (Ioc a✝ b✝).ahb_left:left_lim α (Ioc a✝ b✝).b = α (Ioc a✝ b✝).bhb_right:right_lim α (Ioc a✝ b✝).b = α (Ioc a✝ b✝).b⊢ α[Ioc a✝ b✝]ₗ = α (Ioc a✝ b✝).b - α (Ioc a✝ b✝).a grindAll goals completed! 🐙 | Ioo _ _ =>Iooα:ℝ → ℝa:ℝb:ℝhα:ContinuousOn α ↑(Ioo a b)a✝:ℝb✝:ℝhaa:a < (Ioo a✝ b✝).ahab:(Ioo a✝ b✝).a ≤ (Ioo a✝ b✝).bhbb:(Ioo a✝ b✝).b < bhI:Ioo a✝ b✝ ⊆ Ioo a bha_left:left_lim α (Ioo a✝ b✝).a = α (Ioo a✝ b✝).aha_right:right_lim α (Ioo a✝ b✝).a = α (Ioo a✝ b✝).ahb_left:left_lim α (Ioo a✝ b✝).b = α (Ioo a✝ b✝).bhb_right:right_lim α (Ioo a✝ b✝).b = α (Ioo a✝ b✝).b⊢ α[Ioo a✝ b✝]ₗ = α (Ioo a✝ b✝).b - α (Ioo a✝ b✝).a grindAll goals completed! 🐙 declaration uses 'sorry'example : (fun x ↦ x^2)[Icc 2 2]ₗ = 0 := by⊢ (fun x => x ^ 2)[Icc 2 2]ₗ = 0 sorryAll goals completed! 🐙declaration uses 'sorry'example : (fun x ↦ x^2)[Ioo 2 2]ₗ = 0 := by⊢ (fun x => x ^ 2)[Ioo 2 2]ₗ = 0 sorryAll goals completed! 🐙 theorem BoundedInterval.join_Icc_Ioc' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins' (Icc a b) (Ioc b c) := ⟨ join_Icc_Ioc hab hbc, bya:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ ∀ (α : ℝ → ℝ), α[Icc a c]ₗ = α[Icc a b]ₗ + α[Ioc b c]ₗ simp [α_length, show a ≤ b by grind, show b ≤ c by grind, show a ≤ c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Icc_Ioo' {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ico a c).joins' (Icc a b) (Ioo b c) := ⟨ join_Icc_Ioo hab hbc, bya:ℝb:ℝc:ℝhab:a ≤ bhbc:b < c⊢ ∀ (α : ℝ → ℝ), α[Ico a c]ₗ = α[Icc a b]ₗ + α[Ioo b c]ₗ simp [α_length, show a ≤ b by grind, show b < c by grind, show a ≤ c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Ioc_Ioc' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ioc a c).joins' (Ioc a b) (Ioc b c) := ⟨ join_Ioc_Ioc hab hbc, bya:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ ∀ (α : ℝ → ℝ), α[Ioc a c]ₗ = α[Ioc a b]ₗ + α[Ioc b c]ₗ simp [α_length, show a ≤ b by grind, show b ≤ c by grind, show a ≤ c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Ioc_Ioo' {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ioo a c).joins' (Ioc a b) (Ioo b c) := ⟨ join_Ioc_Ioo hab hbc, bya:ℝb:ℝc:ℝhab:a ≤ bhbc:b < c⊢ ∀ (α : ℝ → ℝ), α[Ioo a c]ₗ = α[Ioc a b]ₗ + α[Ioo b c]ₗ simp [α_length, show a ≤ b by grind, show b < c by grind, show a < c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Ico_Icc' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins' (Ico a b) (Icc b c) := ⟨ join_Ico_Icc hab hbc, bya:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ ∀ (α : ℝ → ℝ), α[Icc a c]ₗ = α[Ico a b]ₗ + α[Icc b c]ₗ simp [α_length, show a ≤ b by grind, show b ≤ c by grind, show a ≤ c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Ico_Ico' {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ico a c).joins' (Ico a b) (Ico b c) := ⟨ join_Ico_Ico hab hbc, bya:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ ∀ (α : ℝ → ℝ), α[Ico a c]ₗ = α[Ico a b]ₗ + α[Ico b c]ₗ simp [α_length, show a ≤ b by grind, show b ≤ c by grind, show a ≤ c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Ioo_Icc' {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioc a c).joins' (Ioo a b) (Icc b c) := ⟨ join_Ioo_Icc hab hbc, bya:ℝb:ℝc:ℝhab:a < bhbc:b ≤ c⊢ ∀ (α : ℝ → ℝ), α[Ioc a c]ₗ = α[Ioo a b]ₗ + α[Icc b c]ₗ simp [α_length, show a < b by grind, show b ≤ c by grind, show a ≤ c by grind]All goals completed! 🐙 ⟩theorem BoundedInterval.join_Ioo_Ico' {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioo a c).joins' (Ioo a b) (Ico b c) := ⟨ join_Ioo_Ico hab hbc, bya:ℝb:ℝc:ℝhab:a < bhbc:b ≤ c⊢ ∀ (α : ℝ → ℝ), α[Ioo a c]ₗ = α[Ioo a b]ₗ + α[Ico b c]ₗ simp [α_length, show a < b by grind, show b ≤ c by grind, show a < c by grind]All goals completed! 🐙 ⟩ noncomputable abbrev P_11_8_6 : Partition (Icc 1 3) := (⊥: Partition (Ico 1 2)).join (⊥ : Partition (Icc 2 3)) (join_Ico_Icc (by⊢ 1 ≤ 2 norm_numAll goals completed! 🐙) (by⊢ 2 ≤ 3 norm_numAll goals completed! 🐙) )theorem declaration uses 'sorry'f_11_8_6_RS_integ : PiecewiseConstantWith.RS_integ f_11_8_6 P_11_8_6 (fun x ↦ x) = 22 := by⊢ (PiecewiseConstantWith.RS_integ f_11_8_6 P_11_8_6 fun x => x) = 22 sorryAll goals completed! 🐙 open Classical in noncomputable abbrev PiecewiseConstantOn.RS_integ (f:ℝ → ℝ) (I: BoundedInterval) (α:ℝ → ℝ): ℝ := if h: PiecewiseConstantOn f I then PiecewiseConstantWith.RS_integ f h.choose α else 0theorem PiecewiseConstantOn.RS_integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: Partition I} (h: PiecewiseConstantWith f P) (α:ℝ → ℝ) : RS_integ f I α = PiecewiseConstantWith.RS_integ f P α := byf:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f Pα:ℝ → ℝ⊢ RS_integ f I α = PiecewiseConstantWith.RS_integ f P α have h' : PiecewiseConstantOn f I := byf:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f Pα:ℝ → ℝ⊢ RS_integ f I α = PiecewiseConstantWith.RS_integ f P α use PAll goals completed! 🐙 simp [RS_integ, h']f:ℝ → ℝI:BoundedIntervalP:Partition Ih:PiecewiseConstantWith f Pα:ℝ → ℝh':Chapter11.PiecewiseConstantOn _fvar.234463 _fvar.234464 := ?_mvar.234473⊢ PiecewiseConstantWith.RS_integ f (Exists.choose ⋯) α = PiecewiseConstantWith.RS_integ f P α; exact PiecewiseConstantWith.RS_integ_eq h'.choose_spec h αAll goals completed! 🐙 open Classical in /-- Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8 -/ theorem declaration uses 'sorry'PiecewiseConstantOn.RS_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J) {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α): PiecewiseConstantOn (fun x ↦ if x ∈ I then f x else 0) J := byI:BoundedIntervalJ:BoundedIntervalhIJ:I ⊆ Jf:ℝ → ℝh:PiecewiseConstantOn f Iα:ℝ → ℝhα:Monotone α⊢ PiecewiseConstantOn (fun x => if x ∈ I then f x else 0) J sorryAll goals completed! 🐙open Classical in /-- Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8 -/ theorem declaration uses 'sorry'PiecewiseConstantOn.RS_integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J) {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α): RS_integ (fun x ↦ if x ∈ I then f x else 0) J α = RS_integ f I α := byI:BoundedIntervalJ:BoundedIntervalhIJ:I ⊆ Jf:ℝ → ℝh:PiecewiseConstantOn f Iα:ℝ → ℝhα:Monotone α⊢ RS_integ (fun x => if x ∈ I then f x else 0) J α = RS_integ f I α sorryAll goals completed! 🐙 noncomputable abbrev lower_RS_integral (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ): ℝ := sSup ((PiecewiseConstantOn.RS_integ ·I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})lemma RS_integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα:Monotone α) : M * α[I]ₗ ∈ (PiecewiseConstantOn.RS_integ ·I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ M * α[I]ₗ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} simpf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ ∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = M * α[I]ₗ; refine ⟨ fun _ ↦ M, ⟨ ⟨ ?_, ?_ ⟩, PiecewiseConstantOn.RS_integ_const M I hα ⟩ ⟩refine_1f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ MajorizesOn (fun x => M) f Irefine_2f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ PiecewiseConstantOn (fun x => M) I .refine_1f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ MajorizesOn (fun x => M) f I grind [abs_le']All goals completed! 🐙 exact (ConstantOn.of_const (c := M) (byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ ∀ x ∈ ↑I, M = M simpAll goals completed! 🐙)).piecewiseConstantOnlemma RS_integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα:Monotone α) : -M * α[I]ₗ ∈ (PiecewiseConstantOn.RS_integ ·I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ -M * α[I]ₗ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} simpf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ ∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = -(M * α[I]ₗ); refine ⟨ fun _ ↦ -M, ⟨ ⟨ ?_, ?_ ⟩, byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ PiecewiseConstantOn.RS_integ (fun x => -M) I α = -(M * α[I]ₗ) convert PiecewiseConstantOn.RS_integ_const _ _ hα using 1h.e'_3f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ -(M * α[I]ₗ) = -M * α[I]ₗ; simpAll goals completed! 🐙 ⟩ ⟩ .refine_1f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ MinorizesOn (fun x => -M) f I grind [abs_le']All goals completed! 🐙 exact (ConstantOn.of_const (c := -M) (byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ Mα:ℝ → ℝhα:Monotone α⊢ ∀ x ∈ ↑I, -M = -M simpAll goals completed! 🐙)).piecewiseConstantOnlemma RS_integral_bound_upper_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) {α:ℝ → ℝ} (hα: Monotone α) : ((PiecewiseConstantOn.RS_integ ·I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty choose M h using hf:ℝ → ℝI:BoundedIntervalα:ℝ → ℝhα:Monotone αM:ℝh:∀ x ∈ ↑I, |f x| ≤ M⊢ ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty; exact Set.nonempty_of_mem (RS_integral_bound_upper_of_bounded h hα)All goals completed! 🐙lemma RS_integral_bound_lower_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) {α:ℝ → ℝ} (hα: Monotone α) : ((PiecewiseConstantOn.RS_integ ·I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty choose M h using hf:ℝ → ℝI:BoundedIntervalα:ℝ → ℝhα:Monotone αM:ℝh:∀ x ∈ ↑I, |f x| ≤ M⊢ ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty; exact Set.nonempty_of_mem (RS_integral_bound_lower_of_bounded h hα)All goals completed! 🐙lemma RS_integral_bound_lower_le_upper {f:ℝ → ℝ} {I: BoundedInterval} {a b:ℝ} {α:ℝ → ℝ} (hα: Monotone α) (ha: a ∈ (PiecewiseConstantOn.RS_integ ·I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) (hb: b ∈ (PiecewiseConstantOn.RS_integ ·I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) : b ≤ a:= byf:ℝ → ℝI:BoundedIntervala:ℝb:ℝα:ℝ → ℝhα:Monotone αha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ b ≤ a have ⟨ g, ⟨ ⟨ hmaj, hgp⟩, hgi ⟩ ⟩ := haf:ℝ → ℝI:BoundedIntervala:ℝb:ℝα:ℝ → ℝhα:Monotone αha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}g:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:(fun x => PiecewiseConstantOn.RS_integ x I α) g = a⊢ b ≤ a have ⟨ h, ⟨ ⟨ hmin, hhp⟩, hhi ⟩ ⟩ := hbf:ℝ → ℝI:BoundedIntervala:ℝb:ℝα:ℝ → ℝhα:Monotone αha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}g:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:(fun x => PiecewiseConstantOn.RS_integ x I α) g = ah:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:(fun x => PiecewiseConstantOn.RS_integ x I α) h = b⊢ b ≤ a rw [←hgi, ←hhi]f:ℝ → ℝI:BoundedIntervala:ℝb:ℝα:ℝ → ℝhα:Monotone αha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}g:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:(fun x => PiecewiseConstantOn.RS_integ x I α) g = ah:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:(fun x => PiecewiseConstantOn.RS_integ x I α) h = b⊢ (fun x => PiecewiseConstantOn.RS_integ x I α) h ≤ (fun x => PiecewiseConstantOn.RS_integ x I α) g; apply hhp.RS_integ_mono hα _ hgpf:ℝ → ℝI:BoundedIntervala:ℝb:ℝα:ℝ → ℝhα:Monotone αha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}g:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:(fun x => PiecewiseConstantOn.RS_integ x I α) g = ah:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:(fun x => PiecewiseConstantOn.RS_integ x I α) h = b⊢ ∀ x ∈ I, h x ≤ g x; intro _ hxf:ℝ → ℝI:BoundedIntervala:ℝb:ℝα:ℝ → ℝhα:Monotone αha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}g:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:(fun x => PiecewiseConstantOn.RS_integ x I α) g = ah:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:(fun x => PiecewiseConstantOn.RS_integ x I α) h = bx✝:ℝhx:x✝ ∈ I⊢ h x✝ ≤ g x✝; linarith [hmin _ hx, hmaj _ hx]All goals completed! 🐙lemma RS_integral_bound_below {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) {α:ℝ → ℝ} (hα: Monotone α) : BddBelow ((PiecewiseConstantOn.RS_integ ·I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ BddBelow ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) rw [bddBelow_def]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ∃ x, ∀ y ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}, x ≤ y; use (RS_integral_bound_lower_nonempty h hα).somehf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ∀ y ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}, ⋯.some ≤ y intro a hahf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone αa:ℝha:a ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ ⋯.some ≤ a; exact RS_integral_bound_lower_le_upper hα ha (RS_integral_bound_lower_nonempty h hα).some_memAll goals completed! 🐙lemma RS_integral_bound_above {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) {α:ℝ → ℝ} (hα: Monotone α): BddAbove ((PiecewiseConstantOn.RS_integ ·I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ BddAbove ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) rw [bddAbove_def]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ∃ x, ∀ y ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}, y ≤ x; use (RS_integral_bound_upper_nonempty h hα).somehf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ∀ y ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}, y ≤ ⋯.some intro b hbhf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone αb:ℝhb:b ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ b ≤ ⋯.some; exact RS_integral_bound_lower_le_upper hα (RS_integral_bound_upper_nonempty h hα).some_mem hbAll goals completed! 🐙lemma le_lower_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα: Monotone α) : -M * α[I]ₗ ≤ lower_RS_integral f I α := ConditionallyCompleteLattice.le_csSup _ _ (RS_integral_bound_above (BddOn.of_bounded h) hα) (RS_integral_bound_lower_of_bounded h hα)lemma lower_RS_integral_le_upper {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) {α:ℝ → ℝ} (hα: Monotone α) : lower_RS_integral f I α ≤ upper_RS_integral f I α := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ lower_RS_integral f I α ≤ upper_RS_integral f I α apply ConditionallyCompleteLattice.csSup_le _ _ (RS_integral_bound_lower_nonempty h hα) _f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ upper_RS_integral f I α ∈ upperBounds ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) rw [mem_upperBounds]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone α⊢ ∀ x ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}, x ≤ upper_RS_integral f I α; introsf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone αx✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ x✝ ≤ upper_RS_integral f I α apply ConditionallyCompleteLattice.le_csInf _ _ (RS_integral_bound_upper_nonempty h hα) _f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone αx✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ x✝ ∈ lowerBounds ((fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) rw [mem_lowerBounds]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone αx✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ ∀ x ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}, x✝ ≤ x; introsf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Iα:ℝ → ℝhα:Monotone αx✝¹:ℝa✝¹:x✝¹ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}x✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ x✝¹ ≤ x✝; solve_by_elim [RS_integral_bound_lower_le_upper]All goals completed! 🐙lemma RS_upper_integral_le {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα: Monotone α) : upper_RS_integral f I α ≤ M * α[I]ₗ := ConditionallyCompleteLattice.csInf_le _ _ (RS_integral_bound_below (.of_bounded h) hα) (RS_integral_bound_upper_of_bounded h hα)lemma upper_RS_integral_le_integ {f g:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I) (hfg: MajorizesOn g f I) (hg: PiecewiseConstantOn g I) {α:ℝ → ℝ} (hα: Monotone α) : upper_RS_integral f I α ≤ PiecewiseConstantOn.RS_integ g I α := ConditionallyCompleteLattice.csInf_le _ _ (RS_integral_bound_below hf hα) ⟨ g, byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfg:MajorizesOn g f Ihg:PiecewiseConstantOn g Iα:ℝ → ℝhα:Monotone α⊢ g ∈ {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} ∧ (fun x => PiecewiseConstantOn.RS_integ x I α) g = PiecewiseConstantOn.RS_integ g I α simpa [hg]All goals completed! 🐙 ⟩lemma integ_le_lower_RS_integral {f h:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I) (hfh: MinorizesOn h f I) (hg: PiecewiseConstantOn h I) {α:ℝ → ℝ} (hα: Monotone α) : PiecewiseConstantOn.RS_integ h I α ≤ lower_RS_integral f I α := ConditionallyCompleteLattice.le_csSup _ _ (RS_integral_bound_above hf hα) ⟨ h, byf:ℝ → ℝh:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfh:MinorizesOn h f Ihg:PiecewiseConstantOn h Iα:ℝ → ℝhα:Monotone α⊢ h ∈ {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} ∧ (fun x => PiecewiseConstantOn.RS_integ x I α) h = PiecewiseConstantOn.RS_integ h I α simpa [hg]All goals completed! 🐙 ⟩lemma lt_of_gt_upper_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I) {α: ℝ → ℝ} (hα: Monotone α) {X:ℝ} (hX: upper_RS_integral f I α < X ) : ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:upper_RS_integral f I α < X⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X have ⟨ Y, hY, hYX ⟩ := exists_lt_of_csInf_lt (RS_integral_bound_upper_nonempty hf hα) hXf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:upper_RS_integral f I α < XY:ℝhY:Y ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hYX:Y < X⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X simp at hYf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:upper_RS_integral f I α < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Y⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X; have ⟨ g, ⟨ hmaj, hgp ⟩, hgi ⟩ := hYf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:upper_RS_integral f I α < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Yg:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:PiecewiseConstantOn.RS_integ g I α = Y⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X; exact ⟨ g, hmaj, hgp, byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:upper_RS_integral f I α < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Yg:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:PiecewiseConstantOn.RS_integ g I α = Y⊢ PiecewiseConstantOn.RS_integ g I α < X rwa [hgi]f:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:upper_RS_integral f I α < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Yg:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ihgi:PiecewiseConstantOn.RS_integ g I α = Y⊢ Y < X ⟩lemma gt_of_lt_lower_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I) {α:ℝ → ℝ} (hα: Monotone α) {X:ℝ} (hX: X < lower_RS_integral f I α) : ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:X < lower_RS_integral f I α⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α have ⟨ Y, hY, hYX ⟩ := exists_lt_of_lt_csSup (RS_integral_bound_lower_nonempty hf hα) hXf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:X < lower_RS_integral f I αY:ℝhY:Y ∈ (fun x => PiecewiseConstantOn.RS_integ x I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}hYX:X < Y⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α simp at hYf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:X < lower_RS_integral f I αY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Y⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α; have ⟨ h, ⟨ hmin, hhp ⟩, hhi ⟩ := hYf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:X < lower_RS_integral f I αY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Yh:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:PiecewiseConstantOn.RS_integ h I α = Y⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α; exact ⟨ h, hmin, hhp, byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:X < lower_RS_integral f I αY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Yh:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:PiecewiseConstantOn.RS_integ h I α = Y⊢ X < PiecewiseConstantOn.RS_integ h I α rwa [hhi]f:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Iα:ℝ → ℝhα:Monotone αX:ℝhX:X < lower_RS_integral f I αY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.RS_integ x I α = Yh:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ihhi:PiecewiseConstantOn.RS_integ h I α = Y⊢ X < Y ⟩ noncomputable abbrev RS_IntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ) : Prop := BddOn f I ∧ lower_RS_integral f I α = upper_RS_integral f I α theorem declaration uses 'sorry'lower_RS_integral_eq_lower_integral (f:ℝ → ℝ) (I: BoundedInterval) : lower_RS_integral f I (fun x ↦ x) = lower_integral f I := byf:ℝ → ℝI:BoundedInterval⊢ (lower_RS_integral f I fun x => x) = lower_integral f I sorryAll goals completed! 🐙theorem declaration uses 'sorry'RS_integ_eq_integ (f:ℝ → ℝ) (I: BoundedInterval) : RS_integ f I (fun x ↦ x) = integ f I := byf:ℝ → ℝI:BoundedInterval⊢ (RS_integ f I fun x => x) = integ f I sorryAll goals completed! 🐙theorem declaration uses 'sorry'RS_IntegrableOn_iff_IntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) : RS_IntegrableOn f I (fun x ↦ x) ↔ IntegrableOn f I := byf:ℝ → ℝI:BoundedInterval⊢ (RS_IntegrableOn f I fun x => x) ↔ IntegrableOn f I sorryAll goals completed! 🐙 end Chapter11