English
For real-analytic style interval integrals with domination, the derivative formula for the integral with respect to x at x0 remains the integral of the derivative at x0.
Русский
Для интегралов по интервалу с доминированием формула производной по x в точке x0 сохраняется как интеграл от производной в x0.
LaTeX
$$$HasFDerivAt\left( x \mapsto \int_{I} F(x,t) d\mu \right)\left(\int_{I} F'(x_0,t) d\mu\right) x_0$$$
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₀`. -/
nonrec theorem hasDerivAt_integral_of_dominated_loc_of_lip {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜} (ε_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_lipsch : ∀ᵐ 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 → HasDerivAt (fun x => F x t) (F' t) x₀) :
IntervalIntegrable F' μ a b ∧ HasDerivAt (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_lipsch h_diff
simp only [intervalIntegrable_iff] at hF_int bound_integrable ⊢
simp only [intervalIntegral_eq_integral_uIoc]
have := hasDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas h_lipsch bound_integrable h_diff
exact ⟨this.1, this.2.const_smul _⟩
