English
In the interval-integral setting, the differentiability under the integral sign holds with the same derivative expression as in the previous interval case.
Русский
В условиях интервалового интеграла дифференцирование под знаком интеграла выполняется и дает тот же выражение производной, что и в предыдущем случае интервала.
LaTeX
$$$HasFDerivAt\left( x \mapsto \int_{t \in I} F(x,t) \; d\mu\right)\left(\int_{I} F'(x_0,t) d\mu\right) x_0$$$
Lean4
/-- Differentiation under integral of `x ↦ ∫ F x a` at a given point `x₀`, assuming
`F x₀` is integrable, `x ↦ F x a` is differentiable on a ball around `x₀` for ae `a` with
derivative norm uniformly bounded by an integrable function (the ball radius is independent of `a`),
and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
nonrec theorem hasFDerivAt_integral_of_dominated_of_fderiv_le {F : H → ℝ → E} {F' : H → ℝ → H →L[𝕜] E} {x₀ : H}
(ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
(hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b)))
(h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t)
(bound_integrable : IntervalIntegrable bound μ a b)
(h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x) :
HasFDerivAt (fun x => ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' x₀ t ∂μ) x₀ :=
by
rw [← ae_restrict_iff' measurableSet_uIoc] at h_bound h_diff
simp only [intervalIntegrable_iff] at hF_int bound_integrable
simp only [intervalIntegral_eq_integral_uIoc]
exact
(hasFDerivAt_integral_of_dominated_of_fderiv_le ε_pos hF_meas hF_int hF'_meas h_bound bound_integrable
h_diff).const_smul
_
