English
Let F: H × ℝ → E and a differentiable in the second variable produce an integral over a real interval; under dominated and measurability assumptions, the derivative with respect to the first variable at x0 exists and equals the interval integral of the derivative at x0.
Русский
Пусть F: H × ℝ → E дифференцируема по первой переменной и интегрируема по t на интервале; при условиях доминирования и измеримости существующая производная по x в точке x0 равна интегралу от производной по x в точке x0 по переменной t.
LaTeX
$$$D_x\Big( x \mapsto \int_{t\in I} F(x,t) \, d\mu(t) \Big)\Big|_{x_0} = \int_{t\in I} F'(x_0,t) \, d\mu(t).$$$
Lean4
/-- Derivative under integral of `x ↦ ∫ F x a` at a given point `x₀ : 𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball around `x₀` for ae `a`
(with ball radius independent of `a`) with integrable Lipschitz bound, and `F x` is
ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
theorem hasDerivAt_integral_of_dominated_loc_of_lip {F' : α → E} (ε_pos : 0 < ε)
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
(hF'_meas : AEStronglyMeasurable F' μ)
(h_lipsch : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs <| bound a) (F · a) (ball x₀ ε))
(bound_integrable : Integrable (bound : α → ℝ) μ) (h_diff : ∀ᵐ a ∂μ, HasDerivAt (F · a) (F' a) x₀) :
Integrable F' μ ∧ HasDerivAt (fun x ↦ ∫ a, F x a ∂μ) (∫ a, F' a ∂μ) x₀ :=
by
set L : E →L[𝕜] 𝕜 →L[𝕜] E := ContinuousLinearMap.smulRightL 𝕜 𝕜 E 1
replace h_diff : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (L (F' a)) x₀ := h_diff.mono fun x hx ↦ hx.hasFDerivAt
have hm : AEStronglyMeasurable (L ∘ F') μ := L.continuous.comp_aestronglyMeasurable hF'_meas
obtain ⟨hF'_int, key⟩ :=
hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hm h_lipsch bound_integrable h_diff
replace hF'_int : Integrable F' μ := by
rw [← integrable_norm_iff hm] at hF'_int
simpa only [L, (· ∘ ·), integrable_norm_iff, hF'_meas, one_mul, norm_one, ContinuousLinearMap.comp_apply,
ContinuousLinearMap.coe_restrict_scalarsL', ContinuousLinearMap.norm_restrictScalars,
ContinuousLinearMap.norm_smulRightL_apply] using hF'_int
refine ⟨hF'_int, ?_⟩
by_cases hE : CompleteSpace E; swap
· simpa [integral, hE] using hasDerivAt_const x₀ 0
simp_rw [hasDerivAt_iff_hasFDerivAt] at h_diff ⊢
simpa only [(· ∘ ·), ContinuousLinearMap.integral_comp_comm _ hF'_int] using key
