English
Extension of differentiation under the integral to interval settings with Lipschitz bounds and ae-measurability assumptions.
Русский
Расширение дифференцирования под интегралом к интервалам с Lipschitz ограничениями и а.е. измеримостью.
LaTeX
$$$$ HasFDerivAt (x \mapsto \int_{a}^{b} F x t \, dt) (\int_{a}^{b} F' t \, dt) x_0 $$$$
Lean4
/-- Differentiation under integral of `x ↦ ∫ x in a..b, F x t` at a given point `x₀ ∈ (a,b)`,
assuming `F x₀` is integrable on `(a,b)`, that `x ↦ F x t` is Lipschitz on a ball around `x₀`
for almost every `t` (with a ball radius independent of `t`) with integrable Lipschitz bound,
and `F x` is a.e.-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
theorem hasFDerivAt_integral_of_dominated_loc_of_lip_interval [NormedSpace ℝ H] {μ : Measure ℝ} {F : H → ℝ → E}
{F' : ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (ε_pos : 0 < ε)
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) <| μ.restrict (Ι a b))
(hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : AEStronglyMeasurable F' <| μ.restrict (Ι a b))
(h_lip : ∀ᵐ t ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs <| bound t) (F · t) (ball x₀ ε))
(bound_integrable : IntervalIntegrable bound μ a b)
(h_diff : ∀ᵐ t ∂μ.restrict (Ι a b), HasFDerivAt (F · t) (F' t) x₀) :
IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀ :=
by
simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
rw [ae_restrict_uIoc_iff] at h_lip h_diff
have H₁ :=
hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas.1 hF_int.1 hF'_meas.1 h_lip.1 bound_integrable.1 h_diff.1
have H₂ :=
hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas.2 hF_int.2 hF'_meas.2 h_lip.2 bound_integrable.2 h_diff.2
exact ⟨⟨H₁.1, H₂.1⟩, H₁.2.sub H₂.2⟩
