English
Under appropriate domination and measurability hypotheses, the map x ↦ ∫ F(x,t) dμ(t) is differentiable at x0 with derivative ∫ F'(x0,t) dμ(t).
Русский
При подходящих условиях доминирования и измеримости отображение x ↦ ∫ F(x,t) dμ(t) дифференцируемо в точке x0, производная равна интегралу от F'(x0,t).
LaTeX
$$$HasFDerivAt\left( x \mapsto \int_{I} F(x,t) \, d\mu(t) \right) \left( \int_{I} F'(x_0,t) \, d\mu(t) \right) (x_0).$$$
Lean4
/-- Differentiation under integral of `x ↦ ∫ t in a..b, F x t` at a given point `x₀`, assuming
`F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball around `x₀` for ae `a`
(with a ball radius independent of `a`) with integrable Lipschitz bound, and `F x` is ae-measurable
for `x` in a possibly smaller neighborhood of `x₀`. -/
nonrec theorem hasFDerivAt_integral_of_dominated_loc_of_lip {F : H → ℝ → E} {F' : ℝ → 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' (μ.restrict (Ι a b)))
(h_lip : ∀ᵐ t ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs <| bound t) (fun x => F x t) (ball x₀ ε))
(bound_integrable : IntervalIntegrable bound μ a b)
(h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x 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
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
simp only [intervalIntegral_eq_integral_uIoc]
have := hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas h_lip bound_integrable h_diff
exact ⟨this.1, this.2.const_smul _⟩
