Analysis I, Section 11.9: The two fundamental theorems of calculus

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:

• The fundamental theorems of calculus.

namespace Chapter11open Chapter9 Chapter10 BoundedInterval theorem declaration uses 'sorry'deriv_of_integ {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) {x₀:ℝ} (hx₀ : x₀ ∈ Set.Icc a b) (hcts: ContinuousWithinAt f (Icc a b) x₀) : HasDerivWithinAt (fun x => integ f (Icc a x)) (f x₀) (.Icc a b) x₀ := bya:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:ContinuousWithinAt f (↑(Icc a b)) x₀⊢ HasDerivWithinAt (fun x => integ f (Icc a x)) (f x₀) (Set.Icc a b) x₀ -- This proof is written to follow the structure of the original text. rw [HasDerivWithinAt.iff_approx_linear]a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:ContinuousWithinAt f (↑(Icc a b)) x₀⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ Set.Icc a b, |x - x₀| < δ → |integ f (Icc a x) - integ f (Icc a x₀) - f x₀ * (x - x₀)| ≤ ε * |x - x₀| simp [(ContinuousWithinAt.tfae _ f hx₀).out 0 2] at hctsa:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < ε⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ Set.Icc a b, |x - x₀| < δ → |integ f (Icc a x) - integ f (Icc a x₀) - f x₀ * (x - x₀)| ≤ ε * |x - x₀| peel hcts with ε hε δ hδ hconvh.h.h.ha:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < ε⊢ ∀ x ∈ Set.Icc a b, |x - x₀| < δ → |integ f (Icc a x) - integ f (Icc a x₀) - f x₀ * (x - x₀)| ≤ ε * |x - x₀|; intro y hy hyδh.h.h.ha:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δ⊢ |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀| obtain hx₀y | rfl | hx₀y := lt_trichotomy x₀ yh.h.h.h.inla:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < y⊢ |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀|h.h.h.h.inr.inla:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εhy:x₀ ∈ Set.Icc a bhyδ:|x₀ - x₀| < δ⊢ |integ f (Icc a x₀) - integ f (Icc a x₀) - f x₀ * (x₀ - x₀)| ≤ ε * |x₀ - x₀|h.h.h.h.inr.inra:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:y < x₀⊢ |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀| .h.h.h.h.inla:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < y⊢ |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀| have := ((hf.join (join_Icc_Ioc hy.1 hy.2)).1.join (join_Icc_Ioc hx₀.1 (le_of_lt hx₀y))).2h.h.h.h.inla:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀| simp [this.2, abs_le', abs_of_pos (show 0 < y - x₀ by linarith)]h.h.h.h.inla:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀) ∧ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y) have h1 := this.1.mono (g := fun _ ↦ f x₀ + ε) (IntegrableOn.const _ _).1 ?_h.h.h.h.inl.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:?_mvar.193198 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀) ∧ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y)h.h.h.h.inl.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ MajorizesOn (fun x => f x₀ + ε) f (Ioc x₀ y) have h2 := (IntegrableOn.const _ _).1.mono (f := fun _ ↦ f x₀ - ε) this.1 ?_h.h.h.h.inl.refine_2.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:?_mvar.193198 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h2:?_mvar.193278 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀) ∧ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y)h.h.h.h.inl.refine_2.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:?_mvar.193198 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ MajorizesOn f (fun x => f x₀ - ε) (Ioc x₀ y)h.h.h.h.inl.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ MajorizesOn (fun x => f x₀ + ε) f (Ioc x₀ y) .h.h.h.h.inl.refine_2.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:?_mvar.193198 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h2:?_mvar.193278 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀) ∧ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y) simp [IntegrableOn.const, le_of_lt hx₀y] at h1 h2h.h.h.h.inl.refine_2.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:integ f (Ioc x₀ y) ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a)h2:(f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) ≤ integ f (Ioc x₀ y)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀) ∧ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y) split_andsh.h.h.h.inl.refine_2.refine_2.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:integ f (Ioc x₀ y) ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a)h2:(f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) ≤ integ f (Ioc x₀ y)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀)h.h.h.h.inl.refine_2.refine_2.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:integ f (Ioc x₀ y) ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a)h2:(f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) ≤ integ f (Ioc x₀ y)⊢ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y) .h.h.h.h.inl.refine_2.refine_2.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:integ f (Ioc x₀ y) ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a)h2:(f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) ≤ integ f (Ioc x₀ y)⊢ integ f (Ioc x₀ y) ≤ ε * (y - x₀) + f x₀ * (y - x₀) convert h1 using 1h.e'_4a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:integ f (Ioc x₀ y) ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a)h2:(f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) ≤ integ f (Ioc x₀ y)⊢ ε * (y - x₀) + f x₀ * (y - x₀) = (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a); ringAll goals completed! 🐙 .h.h.h.h.inl.refine_2.refine_2.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:integ f (Ioc x₀ y) ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a)h2:(f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) ≤ integ f (Ioc x₀ y)⊢ f x₀ * (y - x₀) ≤ ε * (y - x₀) + integ f (Ioc x₀ y) simp [←sub_nonneg] at *h.h.h.h.inl.refine_2.refine_2.refine_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhyδ:|y - x₀| < δhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hx₀:0 ≤ x₀ - a - 0 ∧ 0 ≤ b - x₀ - 0hcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), 0 ≤ x - a - 0 → 0 ≤ b - x - 0 → |x - x₀| < δ → |f x - f x₀| < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), 0 ≤ x - a - 0 → 0 ≤ b - x - 0 → |x - x₀| < δ → |f x - f x₀| < εhy:0 ≤ y - a - 0 ∧ 0 ≤ b - y - 0h1:0 ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) - integ f (Ioc x₀ y) - 0h2:0 ≤ integ f (Ioc x₀ y) - (f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) - 0⊢ 0 ≤ ε * (y - x₀) + integ f (Ioc x₀ y) - f x₀ * (y - x₀) - 0; convert h2 using 1h.e'_4a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhyδ:|y - x₀| < δhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hx₀:0 ≤ x₀ - a - 0 ∧ 0 ≤ b - x₀ - 0hcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), 0 ≤ x - a - 0 → 0 ≤ b - x - 0 → |x - x₀| < δ → |f x - f x₀| < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), 0 ≤ x - a - 0 → 0 ≤ b - x - 0 → |x - x₀| < δ → |f x - f x₀| < εhy:0 ≤ y - a - 0 ∧ 0 ≤ b - y - 0h1:0 ≤ (f x₀ + ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) - integ f (Ioc x₀ y) - 0h2:0 ≤ integ f (Ioc x₀ y) - (f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) - 0⊢ ε * (y - x₀) + integ f (Ioc x₀ y) - f x₀ * (y - x₀) - 0 = integ f (Ioc x₀ y) - (f x₀ - ε) * ((Ioc x₀ y).b - (Ioc x₀ y).a) - 0; ringAll goals completed! 🐙 all_goals intro z hzh.h.h.h.inl.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝhx₀:x₀ ∈ Set.Icc a bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0hconv:∀ (x : ℝ), a ≤ x → x ≤ b → |x - x₀| < δ → |f x - f x₀| < εy:ℝhy:y ∈ Set.Icc a bhyδ:|y - x₀| < δhx₀y:x₀ < ythis:?_mvar.180784 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhz:z ∈ ↑(Ioc x₀ y)⊢ f z ≤ (fun x => f x₀ + ε) z; simp [abs_lt] at *h.h.h.h.inl.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ y⊢ f z ≤ f x₀ + ε; specialize hconv z ?_ ?_ ?_ ?_h.h.h.h.inl.refine_1.specialize_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ y⊢ a ≤ zh.h.h.h.inl.refine_1.specialize_2a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ y⊢ z ≤ bh.h.h.h.inl.refine_1.specialize_3a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ y⊢ x₀ < δ + zh.h.h.h.inl.refine_1.specialize_4a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ y⊢ z - x₀ < δh.h.h.h.inl.refine_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ yhconv:f x₀ < ε + f z ∧ f z - f x₀ < ε⊢ f z ≤ f x₀ + ε <;>h.h.h.h.inl.refine_1.specialize_1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:Chapter11.IntegrableOn _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) ∧ Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.180693) = Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Icc _fvar.162051 _fvar.162056) + Chapter11.integ _fvar.162054 (Chapter11.BoundedInterval.Ioc _fvar.162056 _fvar.180693) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)z:ℝhx₀:a ≤ x₀ ∧ x₀ ≤ bhcts:∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhε:0 < εhδ:0 < δhconv:∀ (x : ℝ), a ≤ x → x ≤ b → x₀ < δ + x → x - x₀ < δ → f x₀ < ε + f x ∧ f x - f x₀ < εhy:a ≤ y ∧ y ≤ bhyδ:x₀ < δ + y ∧ y - x₀ < δhz:x₀ < z ∧ z ≤ y⊢ a ≤ zh.h.h.h.inl.refine_1.specialize_2a:ℝb:ℝhab:a < b