Differentiation under the integral sign
TheoremSmoothness of compactly supported parameter integrals#✓fully proved
The integral p ↦ ∫ x, w x • Ψ (c x, p) ∂μ of a smooth compactly
supported function is smooth in the parameter p.
theorem contDiff_integral_smul_comp_of_contDiff_of_hasCompactSupport
{X : Type uX} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
[SecondCountableTopology X]
(μ : Measure X) [IsFiniteMeasureOnCompacts μ]
{M : Type vM} [NormedAddCommGroup M] [NormedSpace ℝ M]
{P : Type vP} [NormedAddCommGroup P] [NormedSpace ℝ P]
{E : Type vE} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
(c : X → M) (hc : Continuous c) (w : X → ℝ) (hw : Continuous w) (hwc : HasCompactSupport w)
(Ψ : M × P → E) (hΨ : ContDiff ℝ (⊤ : ℕ∞) Ψ) (hΨc : HasCompactSupport Ψ) :
ContDiff ℝ (⊤ : ℕ∞) (fun p : P => ∫ x, w x • Ψ (c x, p) ∂μ)TheoremDifferentiating an integral of a series term by term#●ready to prove
Let \(d \in \mathbb{N}\), let \(\Omega\) be an open subset of \(\mathbb{R}^d\), let \(a < c < b\) be real numbers, and for each \(n \in \mathbb{N}\) let \(f_n : \mathbb{R}^d \times \mathbb{R} \to \mathbb{C}\) be almost everywhere measurable on \(\Omega \times (a, b)\) with respect to Lebesgue measure. Write \(\partial_y f_n(x, y)\) for the derivative of \(t \mapsto f_n(x, t)\) at \(y\), taken to be \(0\) where this derivative does not exist, and give every series that does not converge absolutely the sum \(0\). Assume that: (1) for each \(n\) and almost every \(x \in \Omega\), the function \(y \mapsto f_n(x, y)\) is absolutely continuous on \([a, b]\); (2) each \(\partial_y f_n\) is almost everywhere measurable on \(\Omega \times (a, b)\), the series \(\sum_n |\partial_y f_n(x, y)|\) converges for almost every \((x, y) \in \Omega \times (a, b)\), and its sum is integrable on \(\Omega \times (a, b)\); (3) the series \(\sum_n |f_n(x, c)|\) converges for almost every \(x \in \Omega\), and its sum is integrable on \(\Omega\). Then there is a function \(F : \mathbb{R} \to \mathbb{C}\) such that for almost every \(y \in (a, b)\) the function \(x \mapsto \sum_n f_n(x, y)\) is integrable on \(\Omega\), \(F(y) = \int_\Omega \sum_n f_n(x, y)\, dx\), and \(F\) is differentiable at \(y\) with
The joint measurability of each \(f_n\) is a hypothesis of the source that the first formalization dropped. It is needed: for \(d \ge 1\) and nonempty bounded \(\Omega\), a non-measurable \(f_0\) of modulus one that does not depend on \(y\), with \(f_n = 0\) for \(n \ge 1\), satisfies the other hypotheses but not the conclusion.
MathlibExt.MeasureTheory.DerivIntegralSeriesAbsContWanted.exists_hasDerivAt_integral_tsum_ae · 31 lines
public theorem_wanted exists_hasDerivAt_integral_tsum_ae
{d : ℕ} (Ω : Set (Fin d → ℝ)) (hΩ : IsOpen Ω)
(a b c : ℝ) (hab : a < b) (hac : a < c) (hcb : c < b)
(f : ℕ → (Fin d → ℝ) → ℝ → ℂ)
(h_meas : ∀ n : ℕ,
AEStronglyMeasurable (fun p : (Fin d → ℝ) × ℝ => f n p.1 p.2)
((volume.restrict Ω).prod (volume.restrict (Set.Ioo a b))))
(h_ac : ∀ n : ℕ, ∀ᵐ x ∂(volume.restrict Ω),
AbsolutelyContinuousOnInterval (fun y => f n x y) a b)
(h_deriv_meas : ∀ n : ℕ,
AEStronglyMeasurable (fun p : (Fin d → ℝ) × ℝ =>
deriv (fun y => f n p.1 y) p.2)
((volume.restrict Ω).prod (volume.restrict (Set.Ioo a b))))
(h_deriv_sum_finite_ae :
∀ᵐ p ∂((volume.restrict Ω).prod (volume.restrict (Set.Ioo a b))),
Summable (fun n : ℕ => ‖deriv (fun y => f n p.1 y) p.2‖))
(h_deriv_int :
Integrable (fun p : (Fin d → ℝ) × ℝ =>
∑' n : ℕ, ‖deriv (fun y => f n p.1 y) p.2‖)
((volume.restrict Ω).prod (volume.restrict (Set.Ioo a b))))
(h_at_c_sum_finite_ae :
∀ᵐ x ∂(volume.restrict Ω), Summable (fun n : ℕ => ‖f n x c‖))
(h_at_c :
Integrable (fun x : Fin d → ℝ => ∑' n : ℕ, ‖f n x c‖) (volume.restrict Ω)) :
∃ F : ℝ → ℂ,
(∀ᵐ y ∂(volume.restrict (Set.Ioo a b)),
Integrable (fun x : Fin d → ℝ => ∑' n : ℕ, f n x y) (volume.restrict Ω)) ∧
(∀ᵐ y ∂(volume.restrict (Set.Ioo a b)),
F y = ∫ x, ∑' n : ℕ, f n x y ∂(volume.restrict Ω)) ∧
(∀ᵐ y ∂(volume.restrict (Set.Ioo a b)),
HasDerivAt F (∑' n : ℕ, ∫ x, deriv (fun t => f n x t) y ∂(volume.restrict Ω)) y)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem
ma_proofbench_l2_50, with the change above.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.