English
If hs is convex, and ω is continuously varying near a within s, then the derivative (within s) of the map b ↦ ∫_{segment a to b} ω(x) dx at b = a equals ω(a).
Русский
Если конвексно множество hs и ω непрерывно изменяется рядом с a внутри s, то производная (в пределах s) функции b ↦ ∫_{отрезка a..b} ω(x) dx в точке b = a равна ω(a).
LaTeX
$$$\\text{HasFDerivWithinAt} \\left(\\int_{\\text{segment } a..b} \\omega(x)dx\\right) = \\omega(a) \\quad\\text{at } b=a$$$
Lean4
/-- The integral of `ω` along `[a -[ℝ] b]`, as a function of `b`, has derivative `ω a` at `b = a`.
This is a `HasFDerivWithinAt` version assuming that `ω` is continuous within a convex set `s`
in a neighborhood of `a` within `s`. -/
theorem curveIntegral_segment_source' (hs : Convex ℝ s) (hω : ∀ᶠ x in 𝓝[s] a, ContinuousWithinAt ω s x) (ha : a ∈ s) :
HasFDerivWithinAt (∫ᶜ x in .segment a ·, ω x) (ω a) s a := by
/- Given `ε > 0`, take a number `δ > 0` such that `ω` is continuous on `ball a δ ∩ s`
and `‖ω z - ω a‖ ≤ ε` on this set.
Then for `b ∈ ball a δ ∩ s`, we have
`‖(∫ᶜ x in .segment a b, ω x) - ω a (b - a)‖
= ‖(∫ᶜ x in .segment a b, ω x) - ∫ᶜ x in .segment a b, ω a‖
≤ ∫ x in 0..1, ‖ω x - ω a‖ * ‖b - a‖
≤ ε * ‖b - a‖`
-/
simp only [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO, Path.segment_same, curveIntegral_refl, sub_zero,
Asymptotics.isLittleO_iff]
intro ε hε
obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0, ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε} :=
by
rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff]
exact ⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩
rw [eventually_nhdsWithin_iff]
filter_upwards [Metric.ball_mem_nhds _ hδ₀] with b hb hbs
have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s := ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by simp [*])
rw [← curveIntegral_segment_const, ← curveIntegral_fun_sub]
· refine norm_curveIntegral_segment_le fun z hz ↦ (hδ (hsub hz)).2
· rw [curveIntegrable_segment]
refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_
refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_
· refine hsub <| segment_eq_image_lineMap ℝ a b ▸ mem_image_of_mem _ ht
· rw [mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
exact hs.segment_subset ha hbs
· rw [curveIntegrable_segment]
exact intervalIntegrable_const
