Integrating out one variable preserves Schwartz space

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #126(ii), out of #122.

★★★ SchwartzMap.integralLastCLM — 𝓢(E × ℝ, ℂ) →L[ℂ] 𝓢(E, ℂ), G ↦ fun p => ∫ t, G (p, t). Mathlib has SchwartzMap.integralCLM, which integrates over the whole domain into a scalar, and nothing that integrates out one variable: this is the two-variable gap #121 names, in its integral form. It is what #126 needs, because a composite integral kernel is exactly one variable integrated out of a product of two kernels.

The two halves, and where each comes from

Smoothness is #124 (differentiation under the integral over a finite-dimensional parameter) and decay is #126's gate in that file (norm_iteratedFDeriv_integral_le, the bound at every order). What this file supplies is the bridge from Schwartz data to #124's directional hypotheses:

• ★ fderiv_comp_inl and ★★ iteratedFDeriv_comp_inl — the chain rule through the inclusion y ↦ (y, t), with ★ norm_iteratedFDeriv_comp_inl_le: a derivative in the first factor is no bigger than the full derivative, because the inclusion has norm one;
• prodDirDeriv and ★★ dirDeriv_eq_prodDirDeriv — the directional derivatives, viewed jointly in both variables. This is what makes #124's measurability hypotheses dischargeable: as a function of the integration variable, a directional derivative in the parameter is a slice of something jointly smooth (★ contDiff_prodDirDeriv), hence continuous, hence measurable — including the operator-valued one (hmeasD), which #124's own scope note flags as unavoidable and which nothing had discharged before this file;
• ★★ one_add_norm_pow_mul_norm_iteratedFDeriv_le — the weight transfer: G's decay at two orders apart gives (1 + ‖p‖)ᴺ·‖∂ᵏG(p, t)‖ ≤ 2^(N+2)·S·(1 + t²)⁻¹ with S a single Finset.sup of G's seminorms. The same two-order combination #122's decay half runs on, with the slots swapped, and in a form SchwartzMap.mkCLM can consume;
• ★ one_add_norm_le_of_sub_norm_le — the parameter weight moves between nearby points, which is what lets a bound family that is constant on a ball carry a weight evaluated at the ball's centre.

Honest scope

⚠️ One variable, and it is the last one. 𝓢(E × F, ℂ) → 𝓢(E, ℂ) for a general second factor F is the same proof with (1 + t²)⁻¹ replaced by an integrable profile on F; only F = ℝ is proved here, because that is what a kernel composition integrates over and because the profile is where the measure enters.

⚠️ The constants are not sharp. 2^(2N+2)·π falls out of the route.

⚠️ Nothing here is a Fubini statement. That the iterated integral equals the double integral is a separate step, and the consumer (#126) does it with Mathlib's integral_integral_swap rather than anything in this file.

References: ContDiffParametricIntegralFDeriv.lean (#124 and #126's gate), SchwartzSlice.lean (#121(i), slicing), WeylSmooth.lean (#122, the same two-order decay combination); specs/BACKLOG.md #126, #124, #122, #121.

The inclusion of the first factor

theorem fderiv_comp_inl {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : Differentiable ℝ D) (x : H) (t : ℝ) : fderiv ℝ (fun (y : H) => D (y, t)) x = fderiv ℝ D (x, t) ∘SL ContinuousLinearMap.inl ℝ H ℝ

The chain rule through y ↦ (y, t): every statement below moves between a derivative in the first factor and the full derivative along it.

theorem iteratedFDeriv_comp_inl {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : ContDiff ℝ (↑⊤) D) (t : ℝ) (k : ℕ) (x : H) : iteratedFDeriv ℝ k (fun (y : H) => D (y, t)) x = (iteratedFDeriv ℝ k D (x, t)).compContinuousLinearMap fun (x : Fin k) => ContinuousLinearMap.inl ℝ H ℝ

★★ The iterated chain rule through the inclusion: the derivative in the first factor is the full derivative precomposed with inl in every slot.

theorem norm_inl_le_one {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] : ‖ContinuousLinearMap.inl ℝ H ℝ‖ ≤ 1

The inclusion has norm at most one, so no power of it appears in any bound.

theorem norm_iteratedFDeriv_comp_inl_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : ContDiff ℝ (↑⊤) D) (t : ℝ) (k : ℕ) (x : H) : ‖iteratedFDeriv ℝ k (fun (y : H) => D (y, t)) x‖ ≤ ‖iteratedFDeriv ℝ k D (x, t)‖

★ A derivative in the first factor is no bigger than the full derivative.

The directional derivatives, viewed in both variables

#124's hypotheses ask for the directional derivatives of p ↦ G (p, t) to be measurable in t, including the operator-valued first one. Folding the inclusion into the recursion makes each of them a slice of a jointly smooth function, which is what discharges those hypotheses.

noncomputable def prodDirDeriv {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (D : H × ℝ → E) : List H → H × ℝ → E

The directional derivatives in the first factor, as functions of both variables.

Equations

• prodDirDeriv D [] = D
• prodDirDeriv D (h :: hs) = fun (q : H × ℝ) => (fderiv ℝ (prodDirDeriv D hs) q) (h, 0)

theorem contDiff_prodDirDeriv {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : ContDiff ℝ (↑⊤) D) (hs : List H) : ContDiff ℝ (↑⊤) (prodDirDeriv D hs)

★ Each of them is jointly smooth.

theorem dirDeriv_eq_prodDirDeriv {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : ContDiff ℝ (↑⊤) D) (hs : List H) (x : H) (t : ℝ) : dirDeriv (fun (p : H) (s : ℝ) => D (p, s)) hs x t = prodDirDeriv D hs (x, t)

★★ And they are #124's directional derivatives.

theorem aestronglyMeasurable_dirDeriv_prodMk {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : ContDiff ℝ (↑⊤) D) (hs : List H) (x : H) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => dirDeriv (fun (p : H) (s : ℝ) => D (p, s)) hs x t) MeasureTheory.volume

The measurability hypothesis #124 asks for.

theorem aestronglyMeasurable_fderiv_dirDeriv_prodMk {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : H × ℝ → E} (hD : ContDiff ℝ (↑⊤) D) (hs : List H) (x : H) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => fderiv ℝ (fun (y : H) => dirDeriv (fun (p : H) (s : ℝ) => D (p, s)) hs y t) x) MeasureTheory.volume

The operator-valued measurability hypothesis #124's scope note flags as unavoidable. The inclusion is what makes it a continuity statement about a jointly smooth function.

The decay the bound family needs

theorem one_add_norm_le_of_sub_norm_le {H : Type u_1} [NormedAddCommGroup H] (N : ℕ) {p x : H} (h : ‖x - p‖ ≤ 1) : (1 + ‖p‖) ^ N ≤ 2 ^ N * (1 + ‖x‖) ^ N

The parameter weight moves between nearby points, which is what lets a bound family that is constant on a ball carry a weight evaluated at the ball's centre.

theorem one_add_norm_pow_mul_norm_iteratedFDeriv_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] (G : SchwartzMap (H × ℝ) E) (N k : ℕ) (p : H) (t : ℝ) : (1 + ‖p‖) ^ N * ‖iteratedFDeriv ℝ k ⇑G (p, t)‖ ≤ 2 ^ (N + 2) * ((Finset.Iic (N + 2, k)).sup (schwartzSeminormFamily ℂ (H × ℝ) E)) G * (1 + t ^ 2)⁻¹

★★ The weight transfer. Two orders of G's decay give a bound that already carries a polynomial weight in the parameter and still has an integrable profile in the integration variable — with the constant a single Finset.sup of G's seminorms, which is the shape SchwartzMap.mkCLM consumes.

The partial integral

theorem contDiff_slice_left {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (G : SchwartzMap (H × ℝ) E) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : H) => G (y, t)

Each slice of a Schwartz function is smooth in the first variable, which is #124's smoothness hypothesis.

theorem integrable_slice_left {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] (G : SchwartzMap (H × ℝ) E) (p : H) : MeasureTheory.Integrable (fun (t : ℝ) => G (p, t)) MeasureTheory.volume

The slice is integrable, which every statement below needs.

theorem norm_dirDeriv_slice_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] (G : SchwartzMap (H × ℝ) E) (N : ℕ) (hs : List H) (x : H) (t : ℝ) : ‖dirDeriv (fun (p : H) (s : ℝ) => G (p, s)) hs x t‖ ≤ dirWeight hs * (((1 + ‖x‖) ^ N)⁻¹ * (2 ^ (N + 2) * ((Finset.Iic (N + 2, hs.length)).sup (schwartzSeminormFamily ℂ (H × ℝ) E)) G * (1 + t ^ 2)⁻¹))

★★ The bound family both statements below run on: a directional derivative of the slice, dominated uniformly in the parameter by G's decay with the integrable profile (1 + t²)⁻¹, and carrying whatever polynomial weight in the parameter is asked for.

theorem contDiff_integral_slice {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ H] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] (G : SchwartzMap (H × ℝ) E) (m : ℕ) : ContDiff ℝ ↑m fun (p : H) => ∫ (t : ℝ), G (p, t)

★★ The partial integral is smooth, by #124 with the bound family above — which is uniform in the parameter, so no ball is needed here.

theorem norm_pow_mul_norm_iteratedFDeriv_integral_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ H] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] (G : SchwartzMap (H × ℝ) E) (N k : ℕ) (p : H) : ‖p‖ ^ N * ‖iteratedFDeriv ℝ k (fun (q : H) => ∫ (t : ℝ), G (q, t)) p‖ ≤ 2 ^ (2 * N + 2) * Real.pi * ((Finset.Iic (N + 2, k)).sup (schwartzSeminormFamily ℂ (H × ℝ) E)) G

★★★ The seminorm estimate, which is what makes the partial integral a Schwartz function. The weight is carried by a bound family that is constant on a unit ball of parameters — which is the shape #126's gate consumes — and ∫ (1 + t²)⁻¹ = π finishes it. The right-hand side is linear in a single Finset.sup of G's seminorms, which is what SchwartzMap.mkCLM asks for.

noncomputable def SchwartzMap.integralLastCLM {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ H] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] : SchwartzMap (H × ℝ) E →L[ℂ] SchwartzMap H E

★★★ Integrating out the last variable maps Schwartz space to Schwartz space, continuously and linearly.

Equations

• SchwartzMap.integralLastCLM = SchwartzMap.mkCLM (fun (G : SchwartzMap (H × ℝ) E) (p : H) => ∫ (t : ℝ), G (p, t)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem SchwartzMap.integralLastCLM_apply {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ H] [NormedSpace ℂ E] [SMulCommClass ℝ ℂ E] (G : SchwartzMap (H × ℝ) E) (p : H) : (integralLastCLM G) p = ∫ (t : ℝ), G (p, t)