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 < 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₀ + ε linarithAll goals completed! 🐙 .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₀| simpAll goals completed! 🐙 sorryAll goals completed! 🐙 noncomputable abbrev F_11_9_2 := fun x ↦ integ f_9_8_5 (Icc 0 x)theorem ContinuousOn.of_F_11_9_2 : ContinuousOn F_11_9_2 (.Icc 0 1) := cts_of_integ IntegrableOn.of_f_9_8_5theorem DifferentiableOn.of_F_11_9_2 {x:ℝ} (hx: ¬ ∃ r:ℚ, x = r) (hx': x ∈ Set.Icc 0 1) : DifferentiableWithinAt ℝ F_11_9_2 (.Icc 0 1) x := byx:ℝhx:¬∃ r, x = ↑rhx':x ∈ Set.Icc 0 1⊢ DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) x have := deriv_of_integ (show 0 < 1 byx:ℝhx:¬∃ r, x = ↑rhx':x ∈ Set.Icc 0 1⊢ DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) x norm_numAll goals completed! 🐙) .of_f_9_8_5 hx' (ContinuousAt.of_f_9_8_5 hx).continuousWithinAt rw [hasDerivWithinAt_iff_hasFDerivWithinAt] at thisx:ℝhx:¬∃ r, x = ↑rhx':x ∈ Set.Icc 0 1this:HasFDerivWithinAt (fun x => integ f_9_8_5 (Icc 0 x)) (ContinuousLinearMap.smulRight 1 (f_9_8_5 x)) (Set.Icc 0 1) x⊢ DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) x use (ContinuousLinearMap.smulRight (1:ℝ →L[ℝ] ℝ) (f_9_8_5 x))All goals completed! 🐙 theorem AntiderivOn.mono {F f: ℝ → ℝ} {I J: BoundedInterval} (h: AntiderivOn F f I) (hIJ: J ⊆ I) : AntiderivOn F f J := ⟨ h.1.mono hIJ, byF:ℝ → ℝf:ℝ → ℝI:BoundedIntervalJ:BoundedIntervalh:AntiderivOn F f IhIJ:J ⊆ I⊢ ∀ x ∈ J, HasDerivWithinAt F (f x) (↑J) x intro x hxF:ℝ → ℝf:ℝ → ℝI:BoundedIntervalJ:BoundedIntervalh:AntiderivOn F f IhIJ:J ⊆ Ix:ℝhx:x ∈ J⊢ HasDerivWithinAt F (f x) (↑J) x; rw [subset_iff] at hIJF:ℝ → ℝf:ℝ → ℝI:BoundedIntervalJ:BoundedIntervalh:AntiderivOn F f IhIJ:↑J ⊆ ↑Ix:ℝhx:x ∈ J⊢ HasDerivWithinAt F (f x) (↑J) x; exact (h.2 x (hIJ hx)).mono hIJAll goals completed! 🐙 ⟩ open Realnoncomputable abbrev F_11_9 : ℝ → ℝ := fun x ↦ if x = 0 then 0 else x^2 * sin (1 / x^3)declaration uses 'sorry'example : Differentiable ℝ F_11_9 := by⊢ Differentiable ℝ F_11_9 sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ BddOn (deriv F_11_9) (.Icc (-1) 1) := by⊢ ¬BddOn (deriv F_11_9) (Set.Icc (-1) 1) sorryAll goals completed! 🐙declaration uses 'sorry'example : AntiderivOn F_11_9 (deriv F_11_9) (Icc (-1) 1) := by⊢ AntiderivOn F_11_9 (deriv F_11_9) (Icc (-1) 1) sorryAll goals completed! 🐙 end Chapter11 theorem declaration uses 'sorry'Chapter7.Series.converges_qseries'' (p:ℝ) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ p : Series).absConverges ↔ (p>1) := byp:ℝ⊢ (mk' fun n => 1 / ↑↑n ^ p).absConverges ↔ p > 1 sorryAll goals completed! 🐙