Schwartz Function Slicing and Partial Hermite Coefficients

Defines the slicing of a multi-dimensional Schwartz function along one coordinate and the partial Hermite coefficient map. These are the "A1" and "A2" analytical constructions used in the multi-dimensional Hermite expansion proof.

Main definitions

• euclideanSnoc d y t : embed (y, t) into EuclideanSpace ℝ (Fin (d+1))
• euclideanInit d x : project to the first d coordinates
• schwartzSlice d f y : fix first d+1 coordinates of f ∈ S(ℝ^{d+2}), get S(ℝ)
• schwartzPartialHermiteCoeff d f n : integrate out last coordinate against the n-th Hermite function, get S(ℝ^{d+1})

Sorry inventory

0 sorrys. All lemmas fully proved. <!-- count_axioms:skip -->

Proved lemmas

• euclideanSnoc_norm_sq — ‖euclideanSnoc y t‖² = ‖y‖² + t²
• euclideanSnoc_norm_ge_left — ‖y‖ ≤ ‖euclideanSnoc y t‖
• integral_euclidean_snoc — Fubini for EuclideanSpace slicing
• contDiff_parametric_hermiteCoeff — parametric Hermite coefficient is C^∞
• schwartz_slice_partial_pointwise_bound — pointwise bound via chain rule + CLM norms
• schwartz_slice_partial_seminorm_bound — seminorm bound for scalarized slices

def GaussianField.euclideanSnoc (d : ℕ) (y : EuclideanSpace ℝ (Fin d)) (t : ℝ) : EuclideanSpace ℝ (Fin (d + 1))

Embed EuclideanSpace ℝ (Fin d) × ℝ into EuclideanSpace ℝ (Fin (d + 1)) by appending the real value as the last coordinate.

Equations

• GaussianField.euclideanSnoc d y t = (WithLp.equiv 2 ((i : Fin (d + 1)) → (fun (x : Fin (d + 1)) => ℝ) i)).symm (Fin.snoc (fun (i : Fin d) => y.ofLp i) t)

def GaussianField.euclideanInit (d : ℕ) (x : EuclideanSpace ℝ (Fin (d + 1))) : EuclideanSpace ℝ (Fin d)

Project EuclideanSpace ℝ (Fin (d + 1)) to its first d coordinates.

Equations

• GaussianField.euclideanInit d x = (WithLp.equiv 2 ((i : Fin d) → (fun (x : Fin d) => ℝ) i)).symm fun (i : Fin d) => x.ofLp i.castSucc

theorem GaussianField.euclideanSnoc_init_last (d : ℕ) (x : EuclideanSpace ℝ (Fin (d + 1))) : euclideanSnoc d (euclideanInit d x) (x.ofLp (Fin.last d)) = x

Snoc of init and last coordinate recovers the original point.

noncomputable def GaussianField.schwartzSlice (d : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (y : EuclideanSpace ℝ (Fin (d + 1))) : SchwartzMap ℝ ℝ

Restrict f ∈ S(ℝ^{d+2}) to the hyperplane {x | x_rest = y}, giving a Schwartz function of the last coordinate.

Equations

• GaussianField.schwartzSlice d f y = { toFun := fun (t : ℝ) => f (GaussianField.euclideanSnoc (d + 1) y t), smooth' := ⋯, decay' := ⋯ }

A2: Partial Hermite coefficient is Schwartz

The function g(y) = ∫ f(euclideanSnoc y t) · ψ_n(t) dt is Schwartz in y.

Proof strategy (following the parametric integral approach):

Smoothness (smooth')

Prove ContDiff ℝ m for all m by induction on m:

• Base (m = 0): continuity via continuous_of_dominated
• Step: hasFDerivAt_integral_of_dominated_of_fderiv_le gives the derivative as ∫ (∂_y f)(euclideanSnoc y t) · ψ_n(t) dt, which has the same form with ∂_y f (still Schwartz) replacing f, so the IH applies.

Decay (decay')

Use the key norm bound ‖y‖ ≤ ‖euclideanSnoc y t‖ (euclideanSnoc_norm_ge_left):

1. Commute iteratedFDeriv and the integral (via smooth')
2. Bound ‖y‖^k * |integrand| ≤ ‖euclideanSnoc y t‖^k * |integrand|
3. Apply Schwartz decay of f at the point euclideanSnoc y t
4. The resulting t-integral is finite since hermiteFunction n is integrable.

noncomputable def GaussianField.schwartzPartialHermiteCoeff (d : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (n : ℕ) : SchwartzMap (EuclideanSpace ℝ (Fin (d + 1))) ℝ

Integrate out the last coordinate of f against the n-th Hermite function, giving a Schwartz function of the remaining d + 1 coordinates.

Equations

• GaussianField.schwartzPartialHermiteCoeff d f n = { toFun := fun (y : EuclideanSpace ℝ (Fin (d + 1))) => hermiteCoeff1D n (GaussianField.schwartzSlice d f y), smooth' := ⋯, decay' := ⋯ }

theorem GaussianField.schwartz_partial_hermiteCoeff_eq_1D (d : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (n : ℕ) (y : EuclideanSpace ℝ (Fin (d + 1))) : (schwartzPartialHermiteCoeff d f n) y = hermiteCoeff1D n (schwartzSlice d f y)

theorem GaussianField.schwartz_slice_eq (d : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (y : EuclideanSpace ℝ (Fin (d + 1))) (t : ℝ) : (schwartzSlice d f y) t = f (euclideanSnoc (d + 1) y t)

theorem GaussianField.integral_euclidean_snoc (d : ℕ) (g : EuclideanSpace ℝ (Fin (d + 2)) → ℝ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (x : EuclideanSpace ℝ (Fin (d + 2))), g x = ∫ (y : EuclideanSpace ℝ (Fin (d + 1))) (t : ℝ), g (euclideanSnoc (d + 1) y t)

Fubini theorem for EuclideanSpace slicing. Isolates the measure equivalence between ℝ^{d+2} and ℝ^{d+1} × ℝ.

Scalarization helpers for seminorm control

These helpers reduce the multi-dimensional seminorm control problem to 1D by evaluating the multilinear map D^{l'}_y[g_n] along arbitrary vectors v, reducing to a 1D problem solvable by hermiteCoeff1D_decay.

noncomputable def GaussianField.schwartzSlicePartial (d : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (l' : ℕ) (y : EuclideanSpace ℝ (Fin (d + 1))) (v : Fin l' → EuclideanSpace ℝ (Fin (d + 1))) : SchwartzMap ℝ ℝ

The 1D Schwartz function obtained by evaluating the l'-th iterated Fréchet derivative of a slice along vectors v. Used for the "scalarization" step: reduce the operator norm of D^{l'} g_n(y) to pointwise evaluations that can be bounded via 1D Hermite decay.

Equations

• One or more equations did not get rendered due to their size.

theorem GaussianField.schwartz_partial_hermiteCoeff_iteratedFDeriv (d : ℕ) (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (n l' : ℕ) (y : EuclideanSpace ℝ (Fin (d + 1))) (v : Fin l' → EuclideanSpace ℝ (Fin (d + 1))) : (iteratedFDeriv ℝ l' (⇑(schwartzPartialHermiteCoeff d f n)) y) v = hermiteCoeff1D n (schwartzSlicePartial d f l' y v)

The iterated Fréchet derivative of schwartzPartialHermiteCoeff d f n evaluated at y along vectors v equals the 1D Hermite coefficient of the corresponding slice partial function. This is the key "commutation" lemma that connects the multi-d seminorm to a 1D quantity.

theorem GaussianField.schwartz_slice_partial_seminorm_bound (d k' l' a b : ℕ) : ∃ (C : ℝ) (q' : Finset (ℕ × ℕ)), 0 < C ∧ ∀ (f : SchwartzMap (EuclideanSpace ℝ (Fin (d + 2))) ℝ) (y : EuclideanSpace ℝ (Fin (d + 1))) (v : Fin l' → EuclideanSpace ℝ (Fin (d + 1))), ‖y‖ ^ k' * (schwartzSeminormFamily ℝ ℝ ℝ (a, b)) (schwartzSlicePartial d f l' y v) ≤ (C * ∏ i : Fin l', ‖v i‖) * (q'.sup (schwartzSeminormFamily ℝ (EuclideanSpace ℝ (Fin (d + 2))) ℝ)) f

Seminorm bound for the slice partial function: the 1D Schwartz seminorm of schwartzSlicePartial d f l' y v, weighted by ‖y‖^k', is bounded by a product of ∏ ‖v_i‖ and finitely many higher-dimensional seminorms of f.