Аналіз I, Розділ 11.8: Інтеграл Рімана–Стєльтьєса

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Визначення α-довжини.

• Кусочно постійний інтеграл Рімана–Стєльтьєса.

• Повний інтеграл Рімана–Стєльтьєса.

Технічні примітки:

• У Lean зручніше робити визначення, такі як α-довжина та інтеграл Рімана–Стєльтьєса, повністю визначеними, призначаючи «сміттеві» значення у випадках, коли визначення не призначене для застосування. Для визначення α-довжини його передбачається застосовувати в контекстах, де існують ліві та праві границі, а функція продовжується константами ліворуч і праворуч від своєї передбаченої області визначення; наприклад, якщо функція Unknown identifier `f`f визначена на Unknown identifier `Icc`Icc 0 1, то передбачається, що Unknown identifier `f`sorry = sorry : Propf x = Unknown identifier `f`f 1 для всіх Unknown identifier `x`sorry ≥ 1 : Propx ≥ 1 і Unknown identifier `f`sorry = sorry : Propf x = Unknown identifier `f`f 0 для всіх Unknown identifier `x`sorry ≤ 0 : Propx ≤ 0; зокрема, на правому кінці відрізка значення функції повинно збігатися з її правим границею, і аналогічно для лівого кінця, хоча ми цього не вимагаємо у нашому визначенні α-довжини. (Для функцій, визначених на відкритих проміжках, таке продовження не має значення.)

• Поняття α-довжини та кусочно постійного інтегралу Рімана–Стєльтьєса передбачено для випадків, де існують ліві та праві границі, наприклад, для монотонних або неперервних функцій, хоча технічно вони мають сенс і без цих припущень. Повний інтеграл Рімана–Стєльтьєса призначений для функцій обмеженої варіації, хоча ми переважно зосередимося на спеціальному випадку монотонно зростаючих функцій.

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 /-- Теорема 11.8.8 (g) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 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 /-- Теорема 11.8.8 (g) (Закони інтегрування Рімана–Стєльтьєса) / Вправа 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