Imports
import Mathlib.Tactic
import Mathlib.Topology.ContinuousOn
import Analysis.Section_7_3
import Analysis.Section_9_4
import Analysis.Section_9_8
import Analysis.Section_10_1
import Analysis.Section_10_2
import Analysis.Section_11_6
import Analysis.Section_11_8Analysis 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 BoundedIntervalTheorem 11.9.1 (First Fundamental Theorem of Calculus)
theorem cts_of_integ {a b:ℝ} {f:ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) :
ContinuousOn (fun x => integ f (Icc a x)) (.Icc a b) := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)⊢ ContinuousOn (fun x ↦ integ f (Icc a x)) (Set.Icc a b)
-- This proof is written to follow the structure of the original text.
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)⊢ ContinuousOn F (Set.Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ M⊢ ContinuousOn F (Set.Icc a b)
have {x y:ℝ} (hxy: x < y) (hx: x ∈ Set.Icc a b) (hy: y ∈ Set.Icc a b) : |F y - F x| ≤ M * (y - x) := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)⊢ ContinuousOn (fun x ↦ integ f (Icc a x)) (Set.Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ b⊢ |F y - F x| ≤ M * (y - x)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ |F y - F x| ≤ M * (y - x)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ integ f (Ioc x y) ≤ M * (y - x) ∧ -integ f (Ioc x y) ≤ M * (y - x)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ integ f (Ioc x y) ≤ M * (y - x)a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ -integ f (Ioc x y) ≤ M * (y - x)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ integ f (Ioc x y) ≤ M * (y - x) a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ M * (y - x) = integ (fun x ↦ M) (Ioc x y)a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ MajorizesOn (fun x ↦ M) f (Ioc x y)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ M * (y - x) = integ (fun x ↦ M) (Ioc x y) All goals completed! 🐙
intro z a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)⊢ f z ≤ (fun x ↦ M) z
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)⊢ z ∈ ↑(Icc a b)a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)hM:|f z| ≤ M⊢ f z ≤ (fun x ↦ M) z
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)⊢ z ∈ ↑(Icc a b) a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhM:∀ (x : ℝ), a ≤ x → x ≤ b → |f x| ≤ Mhz:x < z ∧ z ≤ y⊢ a ≤ z ∧ z ≤ b; All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ -(M * (y - x)) ≤ integ f (Ioc x y)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ -(M * (y - x)) = integ (fun x ↦ -M) (Ioc x y)a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ MajorizesOn f (fun x ↦ -M) (Ioc x y)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)⊢ -(M * (y - x)) = integ (fun x ↦ -M) (Ioc x y) All goals completed! 🐙
intro z a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)⊢ (fun x ↦ -M) z ≤ f z
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)⊢ z ∈ ↑(Icc a b)a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)hM:|f z| ≤ M⊢ (fun x ↦ -M) z ≤ f z
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhz:z ∈ ↑(Ioc x y)⊢ z ∈ ↑(Icc a b) a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝx:ℝy:ℝhxy:x < yhx:a ≤ x ∧ x ≤ bhy:a ≤ y ∧ y ≤ bthis:IntegrableOn f (Ioc x y) ∧ integ f (Icc a y) = integ f (Icc a x) + integ f (Ioc x y)z:ℝhM:∀ (x : ℝ), a ≤ x → x ≤ b → |f x| ≤ Mhz:x < z ∧ z ≤ y⊢ a ≤ z ∧ z ≤ b; All goals completed! 🐙
All goals completed! 🐙
replace {x y:ℝ} (hx: x ∈ Set.Icc a b) (hy: y ∈ Set.Icc a b) :
|F y - F x| ≤ M * |x-y| := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)⊢ ContinuousOn (fun x ↦ integ f (Icc a x)) (Set.Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x < y → x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * (y - x)x:ℝy:ℝhx:x ∈ Set.Icc a bhy:y ∈ Set.Icc a bh:x < y⊢ |F y - F x| ≤ M * |x - y|a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x < y → x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * (y - x)x:ℝhx:x ∈ Set.Icc a bhy:x ∈ Set.Icc a b⊢ |F x - F x| ≤ M * |x - x|a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x < y → x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * (y - x)x:ℝy:ℝhx:x ∈ Set.Icc a bhy:y ∈ Set.Icc a bh:y < x⊢ |F y - F x| ≤ M * |x - y|
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x < y → x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * (y - x)x:ℝy:ℝhx:x ∈ Set.Icc a bhy:y ∈ Set.Icc a bh:x < y⊢ |F y - F x| ≤ M * |x - y| All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x < y → x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * (y - x)x:ℝhx:x ∈ Set.Icc a bhy:x ∈ Set.Icc a b⊢ |F x - F x| ≤ M * |x - x| All goals completed! 🐙
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x < y → x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * (y - x)x:ℝy:ℝhx:x ∈ Set.Icc a bhy:y ∈ Set.Icc a bh:y < x⊢ |F y - F x| ≤ M * |x - y| All goals completed! 🐙
replace : UniformContinuousOn F (.Icc a b) := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)⊢ ContinuousOn (fun x ↦ integ f (Icc a x)) (Set.Icc a b)
a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|⊢ ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |x - y| < δ → |F x - F y| < ε
intro ε a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < ε⊢ ∃ δ, 0 < δ ∧ ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |x - y| < δ → |F x - F y| < ε
use (ε/(max M 1)), (a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < ε⊢ 0 < ε / max M 1 All goals completed! 🐙)
intro x a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a b⊢ ∀ y ∈ Set.Icc a b, |x - y| < ε / max M 1 → |F x - F y| < ε a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝ⊢ y ∈ Set.Icc a b → |x - y| < ε / max M 1 → |F x - F y| < ε a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a b⊢ |x - y| < ε / max M 1 → |F x - F y| < ε a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a bhxy:|x - y| < ε / max M 1⊢ |F x - F y| < ε
calc
_ = |F y - F x| := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a bhxy:|x - y| < ε / max M 1⊢ |F x - F y| = |F y - F x| All goals completed! 🐙
_ ≤ M * |x-y| := this hx hy
_ ≤ (max M 1) * |x-y| := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a bhxy:|x - y| < ε / max M 1⊢ M * |x - y| ≤ max M 1 * |x - y| a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a bhxy:|x - y| < ε / max M 1⊢ M ≤ max M 1; All goals completed! 🐙
_ < (max M 1) * (ε / (max M 1)) := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a bhxy:|x - y| < ε / max M 1⊢ max M 1 * |x - y| < max M 1 * (ε / max M 1) All goals completed! 🐙
_ = _ := a:ℝb:ℝf:ℝ → ℝhf:IntegrableOn f (Icc a b)F:ℝ → ℝ := fun x ↦ integ f (Icc a x)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ Mthis:∀ {x y : ℝ}, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |F y - F x| ≤ M * |x - y|ε:ℝhε:0 < εx:ℝhx:x ∈ Set.Icc a by:ℝhy:y ∈ Set.Icc a bhxy:|x - y| < ε / max M 1⊢ max M 1 * (ε / max M 1) = ε All goals completed! 🐙
All goals completed! 🐙theorem 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₀ := a:ℝ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.
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₀|
a:ℝ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₀|
a:ℝ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 a:ℝ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 b⊢ |y - x₀| < δ → |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀| a:ℝ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₀|
a:ℝ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₀|a:ℝ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₀|a:ℝ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₀|
a:ℝ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₀| a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)⊢ |integ f (Icc a y) - integ f (Icc a x₀) - f x₀ * (y - x₀)| ≤ ε * |y - x₀|
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + 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)
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)h1:integ f (Ioc x₀ y) ≤ integ (fun x ↦ f x₀ + ε) (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)a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)⊢ MajorizesOn (fun x ↦ f x₀ + ε) f (Ioc x₀ y)
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)h1:integ f (Ioc x₀ y) ≤ integ (fun x ↦ f x₀ + ε) (Ioc x₀ y)h2:integ (fun x ↦ f x₀ - ε) (Ioc x₀ y) ≤ 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)a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)h1:integ f (Ioc x₀ y) ≤ integ (fun x ↦ f x₀ + ε) (Ioc x₀ y)⊢ MajorizesOn f (fun x ↦ f x₀ - ε) (Ioc x₀ y)a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)⊢ MajorizesOn (fun x ↦ f x₀ + ε) f (Ioc x₀ y)
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)h1:integ f (Ioc x₀ y) ≤ integ (fun x ↦ f x₀ + ε) (Ioc x₀ y)h2:integ (fun x ↦ f x₀ - ε) (Ioc x₀ y) ≤ 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) a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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)
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀)a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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)
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀) a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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); All goals completed! 🐙
a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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) a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhyδ:|y - x₀| < δhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhyδ:|y - x₀| < δhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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; All goals completed! 🐙
all_goals intro z a:ℝ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:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)z:ℝhz:z ∈ ↑(Ioc x₀ y)⊢ f z ≤ (fun x ↦ f x₀ + ε) z; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ + ε; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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 ≤ za:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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 ≤ ba:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ < δ + za:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ < δa:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ + ε a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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 ≤ za:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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 ≤ ba:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ < δ + za:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ < δa:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)x₀:ℝε:ℝδ:ℝy:ℝhx₀y:x₀ < ythis:IntegrableOn f (Ioc x₀ y) ∧ integ f (Icc a y) = integ f (Icc a x₀) + integ f (Ioc x₀ y)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₀ + ε All goals completed! 🐙
a:ℝ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₀| All goals completed! 🐙
All goals completed! 🐙Example 11.9.2
theorem IntegrableOn.of_f_9_8_5 : IntegrableOn f_9_8_5 (Icc 0 1) :=
integ_of_monotone (StrictMonoOn.of_f_9_8_5.mono (⊢ ↑(Icc 0 1) ⊆ Set.univ All goals completed! 🐙)).monotoneOnnoncomputable 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 := x:ℝ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 x:ℝhx:¬∃ r, x = ↑rhx':x ∈ Set.Icc 0 1⊢ DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) x All goals completed! 🐙) .of_f_9_8_5 hx' (ContinuousAt.of_f_9_8_5 hx).continuousWithinAt
x:ℝhx:¬∃ r, x = ↑rhx':x ∈ Set.Icc 0 1this:HasFDerivWithinAt (fun x ↦ integ f_9_8_5 (Icc 0 x)) (ContinuousLinearMap.toSpanSingleton ℝ (f_9_8_5 x)) (Set.Icc 0 1) x⊢ DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) x
All goals completed! 🐙Exercise 11.9.1
theorem DifferentiableOn.of_F_11_9_2' {q:ℚ} (hq: (q:ℝ) ∈ Set.Icc 0 1) : ¬ DifferentiableWithinAt ℝ F_11_9_2 (.Icc 0 1) q := q:ℚhq:↑q ∈ Set.Icc 0 1⊢ ¬DifferentiableWithinAt ℝ F_11_9_2 (Set.Icc 0 1) ↑q All goals completed! 🐙Definition 11.9.3. We drop the requirement that x be a limit point as this makes the Lean arguments slightly cleaner
abbrev AntiderivOn (F f: ℝ → ℝ) (I: BoundedInterval) :=
DifferentiableOn ℝ F I ∧ ∀ x ∈ I, HasDerivWithinAt F (f x) I xtheorem AntiderivOn.mono {F f: ℝ → ℝ} {I J: BoundedInterval}
(h: AntiderivOn F f I) (hIJ: J ⊆ I) : AntiderivOn F f J :=
⟨ h.1.mono hIJ, F:ℝ → ℝf:ℝ → ℝI:BoundedIntervalJ:BoundedIntervalh:AntiderivOn F f IhIJ:J ⊆ I⊢ ∀ x ∈ J, HasDerivWithinAt F (f x) (↑J) x intro x F:ℝ → ℝf:ℝ → ℝI:BoundedIntervalJ:BoundedIntervalh:AntiderivOn F f IhIJ:J ⊆ Ix:ℝhx:x ∈ J⊢ HasDerivWithinAt F (f x) (↑J) x; F:ℝ → ℝf:ℝ → ℝI:BoundedIntervalJ:BoundedIntervalh:AntiderivOn F f IhIJ:↑J ⊆ ↑Ix:ℝhx:x ∈ J⊢ HasDerivWithinAt F (f x) (↑J) x; All goals completed! 🐙 ⟩Theorem 11.9.4 (Second Fundamental Theorem of Calculus)
theorem integ_eq_antideriv_sub {a b:ℝ} (h:a ≤ b) {f F: ℝ → ℝ}
(hf: IntegrableOn f (Icc a b)) (hF: AntiderivOn F f (Icc a b)) :
integ f (Icc a b) = F b - F a := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
-- This proof is written to follow the structure of the original text.
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < b⊢ integ f (Icc a b) = F b - F aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a = b⊢ integ f (Icc a b) = F b - F a
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < b⊢ integ f (Icc a b) = F b - F a have hF_cts : ContinuousOn F (.Icc a b) := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
intro x a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bx:ℝhx:x ∈ Set.Icc a b⊢ ContinuousWithinAt F (Set.Icc a b) x; All goals completed! 🐙
-- for technical reasons we need to extend F by constant outside of Icc a b
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)⊢ integ f (Icc a b) = F b - F a
have hFF' {x:ℝ} (hx: x ∈ Set.Icc a b) : F' x = F x := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a All goals completed! 🐙
have hF'_cts : ContinuousOn F' (Ioo (a-1) (b+1)) := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
convert (hF_cts.comp_continuous (f := fun x ↦ max (min x b) a) (a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F x⊢ Continuous fun x ↦ max (min x b) a All goals completed! 🐙) ?_).continuousOn using 1
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xx✝:ℝ⊢ (fun x ↦ max (min x b) a) x✝ ∈ Set.Icc a b; All goals completed! 🐙
have hupper (P: Partition (Icc a b)) : upper_riemann_sum f P ≥ F b - F a := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ F b - F a
calc
_ ≥ ∑ J ∈ P.intervals, F'[J]ₗ := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ ∑ J ∈ P.intervals, α_length F' J
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ ∀ i ∈ P.intervals, α_length F' i ≤ sSup (f '' ↑i) * i.length
intro J a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervals⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:↑J = ∅⊢ α_length F' J ≤ sSup (f '' ↑J) * J.lengtha:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:¬↑J = ∅⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:↑J = ∅⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:¬↑J = ∅hJab:J.b ≤ J.a⊢ α_length F' J ≤ sSup (f '' ↑J) * J.lengtha:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:¬↑J = ∅hJab:J.a < J.b⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:¬↑J = ∅hJab:J.b ≤ J.a⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJab:J.b ≤ J.ahJ_empty:(↑J).Nonempty⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJab:J.b ≤ J.ax:ℝhx:x ∈ ↑J⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
cases J with
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝa✝:ℝb✝:ℝhJ:Ioo a✝ b✝ ∈ P.intervalshJab:(Ioo a✝ b✝).b ≤ (Ioo a✝ b✝).ahx:x ∈ ↑(Ioo a✝ b✝)⊢ α_length F' (Ioo a✝ b✝) ≤ sSup (f '' ↑(Ioo a✝ b✝)) * (Ioo a✝ b✝).length a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝa✝:ℝb✝:ℝhJ:Ioo a✝ b✝ ∈ P.intervalshJab:(Ioo a✝ b✝).b ≤ (Ioo a✝ b✝).ahx:a✝ < x ∧ x < b✝⊢ α_length F' (Ioo a✝ b✝) ≤ sSup (f '' ↑(Ioo a✝ b✝)) * (Ioo a✝ b✝).length; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝa✝:ℝb✝:ℝhJ:Ioc a✝ b✝ ∈ P.intervalshJab:(Ioc a✝ b✝).b ≤ (Ioc a✝ b✝).ahx:x ∈ ↑(Ioc a✝ b✝)⊢ α_length F' (Ioc a✝ b✝) ≤ sSup (f '' ↑(Ioc a✝ b✝)) * (Ioc a✝ b✝).length a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝa✝:ℝb✝:ℝhJ:Ioc a✝ b✝ ∈ P.intervalshJab:(Ioc a✝ b✝).b ≤ (Ioc a✝ b✝).ahx:a✝ < x ∧ x ≤ b✝⊢ α_length F' (Ioc a✝ b✝) ≤ sSup (f '' ↑(Ioc a✝ b✝)) * (Ioc a✝ b✝).length; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝa✝:ℝb✝:ℝhJ:Ico a✝ b✝ ∈ P.intervalshJab:(Ico a✝ b✝).b ≤ (Ico a✝ b✝).ahx:x ∈ ↑(Ico a✝ b✝)⊢ α_length F' (Ico a✝ b✝) ≤ sSup (f '' ↑(Ico a✝ b✝)) * (Ico a✝ b✝).length a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝa✝:ℝb✝:ℝhJ:Ico a✝ b✝ ∈ P.intervalshJab:(Ico a✝ b✝).b ≤ (Ico a✝ b✝).ahx:a✝ ≤ x ∧ x < b✝⊢ α_length F' (Ico a✝ b✝) ≤ sSup (f '' ↑(Ico a✝ b✝)) * (Ico a✝ b✝).length; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJ:Icc c d ∈ P.intervalshJab:(Icc c d).b ≤ (Icc c d).ahx:x ∈ ↑(Icc c d)⊢ α_length F' (Icc c d) ≤ sSup (f '' ↑(Icc c d)) * (Icc c d).length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJ:Icc c d ∈ P.intervalshJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ d⊢ α_length F' (Icc c d) ≤ sSup (f '' ↑(Icc c d)) * (Icc c d).length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJ:Icc c d ∈ P.intervalshJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ d⊢ α_length F' (Icc d d) ≤ 0
have hnhds: (Ioo (a-1) (b+1):Set ℝ) ∈ nhds d := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ ∑ J ∈ P.intervals, α_length F' J
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:Icc c d ⊆ Icc a b⊢ ↑(Ioo (a - 1) (b + 1)) ∈ nhds d
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:Set.Icc c d ⊆ Set.Icc a b⊢ ↑(Ioo (a - 1) (b + 1)) ∈ nhds d
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:a ≤ c ∧ d ≤ b⊢ ↑(Ioo (a - 1) (b + 1)) ∈ nhds d
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:a ≤ c ∧ d ≤ b⊢ a - 1 < da:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:a ≤ c ∧ d ≤ b⊢ d < b + 1 a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:a ≤ c ∧ d ≤ b⊢ a - 1 < da:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x:ℝc:ℝd:ℝhJab:(Icc c d).b ≤ (Icc c d).ahx:c ≤ x ∧ x ≤ dhJ:a ≤ c ∧ d ≤ b⊢ d < b + 1 All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:¬↑J = ∅c:ℝ := J.ahJab:c < J.b⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ:J ∈ P.intervalshJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < d⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a b⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
have hJ' : Icc a b ⊆ Ioo (a-1/2) (b+1/2) := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ ∑ J ∈ P.intervals, α_length F' J a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a b⊢ a - 1 / 2 < aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a b⊢ b < b + 1 / 2 a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a b⊢ a - 1 / 2 < aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a b⊢ b < b + 1 / 2 All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':Ioo J.a J.b ⊆ Ioo (a - 1 / 2) (b + 1 / 2)⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':Set.Ioo J.a J.b ⊆ Set.Ioo (a - 2⁻¹) (b + 2⁻¹)⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
have hJ'' : Icc a b ⊆ Ioo (a-1) (b+1) := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ ∑ J ∈ P.intervals, α_length F' J a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹⊢ a - 1 < aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹⊢ b < b + 1 a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹⊢ a - 1 < aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹⊢ b < b + 1 All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ α_length F' J ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.lengtha:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ a - 1 < J.aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ J.b < b + 1 a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.lengtha:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ a - 1 < J.aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ J.b < b + 1 try All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)this:∃ x ∈ Set.Ioo c d, HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) x⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.lengtha:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ Set.Icc c d ⊆ ↑(Ioo (a - 1) (b + 1))a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ DifferentiableOn ℝ F' (Set.Ioo c d)
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)this:∃ x ∈ Set.Ioo c d, HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) x⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.length a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) e⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.length
have : HasDerivWithinAt F' (f e) (.Ioo c d) e := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ ∑ J ∈ P.intervals, α_length F' J
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ehJ:Ioo J.a J.b ⊆ Icc a b⊢ HasDerivWithinAt F' (f e) (Set.Ioo c d) e
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ehJ:Set.Ioo J.a J.b ⊆ Set.Icc a b⊢ HasDerivWithinAt F' (f e) (Set.Ioo c d) e
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ehJ:Set.Ioo J.a J.b ⊆ Set.Icc a b⊢ ∀ x ∈ Set.Ioo J.a J.b, F' x = F xa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ehJ:Set.Ioo J.a J.b ⊆ Set.Icc a b⊢ F' e = F e
all_goals All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.lengtha:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) e⊢ ClusterPt e (Filter.principal (Set.Ioo c d \ {e}))
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ F' J.b - F' J.a ≤ sSup (f '' ↑J) * J.length calc
_ = F' d - F' c := rfl
_ = (d - c) * f e := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ F' d - F' c = (d - c) * f e
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ F' d - F' c = (d - c) * ((F' d - F' c) / (d - c)); have : d-c > 0 := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ F' d - F' c = (d - c) * f e All goals completed! 🐙
All goals completed! 🐙
_ = f e * |J|ₗ := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ (d - c) * f e = f e * J.length a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ d - c = max (J.b - J.a) 0 ∨ f e = 0; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ d - c = max (J.b - J.a) 0; All goals completed! 🐙
_ ≤ _ := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ f e * J.length ≤ sSup (f '' ↑J) * J.length
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ f e ≤ sSup (f '' ↑J); a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ BddAbove (f '' ↑J)a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ f e ∈ f '' ↑J
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ BddAbove (f '' ↑J) a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ ∃ x, ∀ y ∈ f '' ↑J, y ≤ x
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ M⊢ ∃ x, ∀ y ∈ f '' ↑J, y ≤ x; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ M⊢ ∀ y ∈ f '' ↑J, y ≤ M
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)M:ℝhM:∀ x ∈ Set.Icc a b, f x ≤ M ∧ -f x ≤ M⊢ ∀ a ∈ ↑J, f a ≤ M
intro x a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)M:ℝhM:∀ x ∈ Set.Icc a b, f x ≤ M ∧ -f x ≤ Mx:ℝhx:x ∈ ↑J⊢ f x ≤ M; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:↑J ⊆ ↑(Icc a b)hJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)M:ℝhM:∀ x ∈ Set.Icc a b, f x ≤ M ∧ -f x ≤ Mx:ℝhx:x ∈ ↑J⊢ f x ≤ M; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:↑J ⊆ ↑(Icc a b)hJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)M:ℝx:ℝhx:x ∈ ↑JhM:f x ≤ M ∧ -f x ≤ M⊢ f x ≤ M; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ ∃ x ∈ ↑J, f x = f e; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ e ∈ ↑J ∧ f e = f e; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:f e = (F' d - F' c) / (d - c)⊢ e ∈ ↑J; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) e⊢ e ∈ closure (Set.Ioo c d \ {e})
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) e⊢ Set.Ioo e d ⊆ Set.Ioo c d \ {e}a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) e⊢ e ∈ closure (Set.Ioo e d)
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) e⊢ Set.Ioo e d ⊆ Set.Ioo c d \ {e} intro _ a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhe:e ∈ Set.Ioo c dhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝa✝:a✝¹ ∈ Set.Ioo e d⊢ a✝¹ ∈ Set.Ioo c d \ {e}; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ (c < a✝¹ ∧ a✝¹ < d) ∧ ¬a✝¹ = e; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ c < a✝¹a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ a✝¹ < da:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ ¬a✝¹ = e a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ c < a✝¹a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ a✝¹ < da:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ea✝¹:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))hJ':a ≤ c + 2⁻¹ ∧ d ≤ b + 2⁻¹he:c < e ∧ e < da✝:e < a✝¹ ∧ a✝¹ < d⊢ ¬a✝¹ = e All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ehe:c < e ∧ e < d⊢ e ∈ closure (Set.Ioo e d); a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ehe:c < e ∧ e < d⊢ e ∈ Set.Icc e d; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this✝:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)e:ℝhmean:HasDerivWithinAt F' ((F' d - F' c) / (d - c)) (Set.Ioo c d) ethis:HasDerivWithinAt F' (f e) (Set.Ioo c d) ehe:c < e ∧ e < d⊢ e ≤ d; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ Set.Icc c d ⊆ ↑(Ioo (a - 1) (b + 1)) a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ Set.Icc c d ⊆ Set.Ioo (a - 1) (b + 1); a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ:J ⊆ Icc a bhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)⊢ a - 1 < c ∧ d < b + 1; All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)hJ:Ioo J.a J.b ⊆ Icc a b⊢ DifferentiableOn ℝ F' (Set.Ioo c d)
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)hJ:Ioo J.a J.b ⊆ Icc a b⊢ ∀ x ∈ Set.Ioo c d, F' x = F xa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)hJ:Ioo J.a J.b ⊆ Icc a b⊢ Set.Ioo c d ⊆ ↑(Icc a b)
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)hJ:Ioo J.a J.b ⊆ Icc a b⊢ ∀ x ∈ Set.Ioo c d, F' x = F x intro x a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)hJ:Ioo J.a J.b ⊆ Icc a bx:ℝhx:x ∈ Set.Ioo c d⊢ F' x = F x
have : x ∈ Set.Icc a b := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ upper_riemann_sum f P ≥ ∑ J ∈ P.intervals, α_length F' J a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)J:BoundedIntervalhJ_empty:¬↑J = ∅c:ℝ := J.ad:ℝ := J.bhJab:c < dhJ':a - 2⁻¹ ≤ c ∧ d ≤ b + 2⁻¹hJ'':J ⊆ Ioo (a - 1) (b + 1)x:ℝhx:x ∈ Set.Ioo c dhJ:x ∈ Icc a b⊢ x ∈ Set.Icc a b; All goals completed! 🐙
All goals completed! 🐙
All goals completed! 🐙
_ = F'[Icc a b]ₗ := P.sum_of_α_length F'
_ = F' b - F' a := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ α_length F' (Icc a b) = F' b - F' a
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ a - 1 < (Icc a b).aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ (Icc a b).a ≤ (Icc a b).ba:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ (Icc a b).b < b + 1a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ Icc a b ⊆ Ioo (a - 1) (b + 1) a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ a - 1 < (Icc a b).aa:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ (Icc a b).a ≤ (Icc a b).ba:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ (Icc a b).b < b + 1a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ Icc a b ⊆ Ioo (a - 1) (b + 1) try a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ Icc a b ⊆ Ioo (a - 1) (b + 1)
intro _ a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x✝:ℝa✝:x✝ ∈ Icc a b⊢ x✝ ∈ Ioo (a - 1) (b + 1); a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)x✝:ℝhFF':∀ {x : ℝ}, a ≤ x → x ≤ b → F' x = F xhF'_cts:ContinuousOn F' (Set.Ioo (a - 1) (b + 1))a✝:a ≤ x✝ ∧ x✝ ≤ b⊢ a - 1 < x✝ ∧ x✝ < b + 1; All goals completed! 🐙
_ = _ := a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ F' b - F' a = F b - F a a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ F' b = F ba:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ F' a = F a a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ F' b = F ba:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ F' a = F a a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ a ∈ Set.Icc a b a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ b ∈ Set.Icc a ba:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))P:Partition (Icc a b)this:∑ J ∈ P.intervals, α_length F' J = α_length F' (Icc a b)⊢ a ∈ Set.Icc a b All goals completed! 🐙
have hlower (P: Partition (Icc a b)) : lower_riemann_sum f P ≤ F b - F a := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
All goals completed! 🐙
replace hupper : upper_integral f (Icc a b) ≥ F b - F a := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hupper:∀ (P : Partition (Icc a b)), upper_riemann_sum f P ≥ F b - F ahlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F a⊢ sInf (Set.range fun P ↦ upper_riemann_sum f P) ≥ F b - F a; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hupper:∀ (P : Partition (Icc a b)), upper_riemann_sum f P ≥ F b - F ahlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F a⊢ (Set.range fun P ↦ upper_riemann_sum f P).Nonemptya:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hupper:∀ (P : Partition (Icc a b)), upper_riemann_sum f P ≥ F b - F ahlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F a⊢ ∀ b_1 ∈ Set.range fun P ↦ upper_riemann_sum f P, F b - F a ≤ b_1 a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hupper:∀ (P : Partition (Icc a b)), upper_riemann_sum f P ≥ F b - F ahlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F a⊢ (Set.range fun P ↦ upper_riemann_sum f P).Nonemptya:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hupper:∀ (P : Partition (Icc a b)), upper_riemann_sum f P ≥ F b - F ahlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F a⊢ ∀ b_1 ∈ Set.range fun P ↦ upper_riemann_sum f P, F b - F a ≤ b_1 a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hupper:∀ (P : Partition (Icc a b)), upper_riemann_sum f P ≥ F b - F ahlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F a⊢ ∀ (a_1 : Partition (Icc a b)), F b ≤ upper_riemann_sum f a_1 + F a
All goals completed! 🐙
replace hlower : lower_integral f (Icc a b) ≤ F b - F a := a:ℝb:ℝh:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)⊢ integ f (Icc a b) = F b - F a
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F ahupper:upper_integral f (Icc a b) ≥ F b - F a⊢ sSup (Set.range fun P ↦ lower_riemann_sum f P) ≤ F b - F a; a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F ahupper:upper_integral f (Icc a b) ≥ F b - F a⊢ (Set.range fun P ↦ lower_riemann_sum f P).Nonemptya:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F ahupper:upper_integral f (Icc a b) ≥ F b - F a⊢ ∀ b_1 ∈ Set.range fun P ↦ lower_riemann_sum f P, b_1 ≤ F b - F a a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F ahupper:upper_integral f (Icc a b) ≥ F b - F a⊢ (Set.range fun P ↦ lower_riemann_sum f P).Nonemptya:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F ahupper:upper_integral f (Icc a b) ≥ F b - F a⊢ ∀ b_1 ∈ Set.range fun P ↦ lower_riemann_sum f P, b_1 ≤ F b - F a a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a < bhF_cts:ContinuousOn F (Set.Icc a b)F':ℝ → ℝ := fun x ↦ F (max (min x b) a)hFF':∀ {x : ℝ}, x ∈ Set.Icc a b → F' x = F xhF'_cts:ContinuousOn F' ↑(Ioo (a - 1) (b + 1))hlower:∀ (P : Partition (Icc a b)), lower_riemann_sum f P ≤ F b - F ahupper:upper_integral f (Icc a b) ≥ F b - F a⊢ ∀ (a_1 : Partition (Icc a b)), lower_riemann_sum f a_1 ≤ F b - F a
All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a = b⊢ integ f (Icc b b) = 0; exact (integ_on_subsingleton (a:ℝb:ℝh✝:a ≤ bf:ℝ → ℝF:ℝ → ℝhf:IntegrableOn f (Icc a b)hF:AntiderivOn F f (Icc a b)h:a = b⊢ (Icc b b).length = 0 All goals completed! 🐙)).2open Realnoncomputable abbrev F_11_9 : ℝ → ℝ := fun x ↦ if x = 0 then 0 else x^2 * sin (1 / x^3)example : Differentiable ℝ F_11_9 := ⊢ Differentiable ℝ F_11_9 All goals completed! 🐙example : ¬ BddOn (deriv F_11_9) (.Icc (-1) 1) := ⊢ ¬BddOn (deriv F_11_9) (Set.Icc (-1) 1) All goals completed! 🐙example : AntiderivOn F_11_9 (deriv F_11_9) (Icc (-1) 1) := ⊢ AntiderivOn F_11_9 (deriv F_11_9) (Icc (-1) 1) All goals completed! 🐙Lemma 11.9.5 / Exercise 11.9.2
theorem antideriv_eq_antideriv_add_const {I:BoundedInterval} {f F G : ℝ → ℝ}
(hfF: AntiderivOn F f I) (hfG: AntiderivOn G f I) :
∃ C, ∀ x ∈ (I:Set ℝ), F x = G x + C := I:BoundedIntervalf:ℝ → ℝF:ℝ → ℝG:ℝ → ℝhfF:AntiderivOn F f IhfG:AntiderivOn G f I⊢ ∃ C, ∀ x ∈ ↑I, F x = G x + C
All goals completed! 🐙/-- Exercise 11.9.3 -/
example {a b x₀:ℝ} (hab: a < b) (hx₀: x₀ ∈ Icc a b) {f: ℝ → ℝ} (hf: MonotoneOn f (Icc a b)) :
DifferentiableWithinAt ℝ (fun x => integ f (Icc a x)) (Icc a b) x₀ ↔
ContinuousWithinAt f (Icc a b) x₀ := a:ℝb:ℝx₀:ℝhab:a < bhx₀:x₀ ∈ Icc a bf:ℝ → ℝhf:MonotoneOn f ↑(Icc a b)⊢ DifferentiableWithinAt ℝ (fun x ↦ integ f (Icc a x)) (↑(Icc a b)) x₀ ↔ ContinuousWithinAt f (↑(Icc a b)) x₀
All goals completed! 🐙end Chapter11Exercise 11.6.5, moved to Section 11.9
theorem Chapter7.Series.converges_qseries' (p:ℝ) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ p : Series).converges ↔ (p>1) := p:ℝ⊢ (mk' fun n ↦ 1 / ↑↑n ^ p).converges ↔ p > 1
All goals completed! 🐙theorem Chapter7.Series.converges_qseries'' (p:ℝ) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ) ^ p : Series).absConverges ↔ (p>1) := p:ℝ⊢ (mk' fun n ↦ 1 / ↑↑n ^ p).absConverges ↔ p > 1
All goals completed! 🐙