English
Under the standard dominated convergence framework, the derivative of a parametric integral with respect to the spatial variable equals the integral of the derivative at the base point.
Русский
При стандартной схеме доминированной конвергенции производная параметрического интеграла по пространственной переменной равна интегралу от производной в базовой точке.
LaTeX
$$$D_x\left( x \mapsto \int F(x,a) \, d\mu(a) \right)\Big|_{x_0} = \int F'(x_0,a) \, d\mu(a).$$$
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 differentiable on an interval around `x₀` for ae `a`
(with interval radius independent of `a`) with derivative uniformly bounded by an integrable
function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
nonrec theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le {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' 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₀ ε, HasDerivAt (fun x => F x t) (F' x t) x) :
IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (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]
have := hasDerivAt_integral_of_dominated_loc_of_deriv_le ε_pos hF_meas hF_int hF'_meas h_bound bound_integrable h_diff
exact ⟨this.1, this.2.const_smul _⟩
