Schwartz Decay Definitions and Integrability Helpers

Defines UniformSchwartzDecay (uniform-in-x Schwartz-class decay in velocity) and proves basic integrability lemmas. This is the standard regularity assumption for kinetic theory used throughout the Coulomb concrete theorem files.

structure VML.UniformSchwartzDecay (f : Torus3 → (Fin 3 → ℝ) → ℝ) : Prop

Uniform C² velocity decay: f(x,·) and its first two velocity derivatives decay faster than any polynomial in |v|, uniformly in x ∈ T³.

This is weaker than Schwartz class (which requires ALL derivatives to decay). The proof of the H-theorem only uses derivatives up to order 2.

• hDecay (N : ℕ) {k : ℕ} : k ≤ 2 → ∃ C > 0, ∀ (x : Torus3) (v : Fin 3 → ℝ), ‖iteratedFDeriv ℝ k (f x) v‖ * (1 + ‖v‖) ^ N ≤ C

  Velocity derivatives up to order 2 of f decay faster than any polynomial, uniformly in x

• hGradDecay (N : ℕ) (i : Fin 3) : ∃ C > 0, ∀ (x : Torus3) (v : Fin 3 → ℝ), |torusGradX (fun (y : Torus3) => f y v) x i| * (1 + ‖v‖) ^ N ≤ C

  Spatial gradients of f also have Schwartz decay in v

theorem VML.inverse_poly_integrable (C : ℝ) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => C / (1 + ‖v‖) ^ 4) MeasureTheory.volume

theorem VML.UniformSchwartzDecay.integrable {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hS : UniformSchwartzDecay f) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (x : Torus3) : MeasureTheory.Integrable (f x) MeasureTheory.volume

Schwartz decay implies integrability.

theorem VML.UniformSchwartzDecay.integrable_poly_mul {f : Torus3 → (Fin 3 → ℝ) → ℝ} (hS : UniformSchwartzDecay f) (hf_smooth : ∀ (x : Torus3), ContDiff ℝ 3 (f x)) (x : Torus3) (M : ℕ) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (1 + ‖v‖) ^ M * f x v) MeasureTheory.volume

Schwartz decay implies integrability with polynomial weight. If f(x,·) decays faster than any polynomial, then (1+‖v‖)^M * |f(x,v)| is integrable for any M.

theorem VML.integrable_one_add_norm_pow_mul {α : Type u_1} [MeasureTheory.MeasureSpace α] [SeminormedAddCommGroup α] {φ : α → ℝ} (hφ : ∀ (k : ℕ), MeasureTheory.Integrable (fun (v : α) => ‖v‖ ^ k * |φ v|) MeasureTheory.volume) (K : ℕ) : MeasureTheory.Integrable (fun (v : α) => (1 + ‖v‖) ^ K * |φ v|) MeasureTheory.volume

If ‖v‖^k * |φ(v)| is integrable for every k, then (1+‖v‖)^K * |φ(v)| is too. Uses the binomial theorem to expand (1+‖v‖)^K as a finite sum. Generalized to any normed space (dimension-independent).

theorem VML.integrable_of_schwartz_bound {α : Type u_1} [MeasureTheory.MeasureSpace α] [SeminormedAddCommGroup α] {φ : α → ℝ} (hφ : ∀ (k : ℕ), MeasureTheory.Integrable (fun (v : α) => ‖v‖ ^ k * |φ v|) MeasureTheory.volume) {g : α → ℝ} (hg_meas : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) {C : ℝ} : 0 ≤ C → ∀ {K : ℕ} (hbound : ∀ (v : α), ‖g v‖ ≤ C * (1 + ‖v‖) ^ K * |φ v|), MeasureTheory.Integrable g MeasureTheory.volume

If ‖v‖^k * |φ(v)| is integrable for every k, and ‖g(v)‖ ≤ C*(1+‖v‖)^K*|φ(v)|, then g is integrable. Core tool for Schwartz-dominance arguments. Generalized to any normed space (dimension-independent).

theorem VML.schwartz_pointwise_decay {α : Type u_1} [NormedAddCommGroup α] [NormedSpace ℝ α] {f : α → ℝ} (hf_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : α), ‖iteratedFDeriv ℝ k f v‖ * (1 + ‖v‖) ^ N ≤ C) (N : ℕ) : ∃ C > 0, ∀ (w : α), |f w| * (1 + ‖w‖) ^ N ≤ C

Extract pointwise (k=0) decay from the Schwartz hypothesis. Generalized to any normed space (dimension-independent).

theorem VML.schwartz_fderiv_component_decay {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf_schwartz : ∀ (N : ℕ) {k : ℕ}, k ≤ 2 → ∃ C > 0, ∀ (v : Fin n → ℝ), ‖iteratedFDeriv ℝ k f v‖ * (1 + ‖v‖) ^ N ≤ C) (j : Fin n) (N : ℕ) : ∃ C > 0, ∀ (w : Fin n → ℝ), |(fderiv ℝ f w) (Pi.single j 1)| * (1 + ‖w‖) ^ N ≤ C

Extract partial derivative (k=1) decay from the Schwartz hypothesis. Generalized to Fin n → ℝ (dimension-independent).

theorem VML.score_bound_of_grad_bound {f : (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_smooth : ContDiff ℝ 3 f) {Cg : ℝ} {Kg : ℕ} (hGrad : ∀ (v : Fin 3 → ℝ) (i : Fin 3), |(fderiv ℝ f v) (Pi.single i 1)| ≤ Cg * (1 + ‖v‖) ^ Kg * f v) (u : Fin 3 → ℝ) (i : Fin 3) : |vGrad (Real.log ∘ f) u i| ≤ Cg * (1 + ‖u‖) ^ Kg

Score bound: |∂_i log f(u)| ≤ Cg * (1+‖u‖)^Kg from the gradient bound on f. Uses chain rule: ∂_i(log∘f) = (∂_if)/f, combined with |∂_if| ≤ Cg*(1+‖u‖)^Kg*f.

theorem VML.schwartz_poly_weighted_decay {α : Type u_1} [SeminormedAddCommGroup α] {f : α → ℝ} (hf_decay : ∀ (N : ℕ), ∃ C > 0, ∀ (w : α), |f w| * (1 + ‖w‖) ^ N ≤ C) (M N : ℕ) : ∃ C > 0, ∀ (w : α), |(1 + ‖w‖) ^ M * f w| * (1 + ‖w‖) ^ N ≤ C

Polynomial-weighted Schwartz decay: if |f(w)|*(1+‖w‖)^N ≤ C for all N, then |(1+‖w‖)^M * f(w)| * (1+‖w‖)^N ≤ C' for all N. Generalized to any normed space (dimension-independent).

theorem VML.schwartz_poly_mul_integrable {f : (Fin 3 → ℝ) → ℝ} (hf_pos : ∀ (v : Fin 3 → ℝ), 0 < f v) (hf_cont : Continuous f) (hf_decay : ∀ (N : ℕ), ∃ C > 0, ∀ (v : Fin 3 → ℝ), |f v| * (1 + ‖v‖) ^ N ≤ C) (K : ℕ) : MeasureTheory.Integrable (fun (v : Fin 3 → ℝ) => (1 + ‖v‖) ^ K * f v) MeasureTheory.volume

Polynomial-weighted Schwartz functions are integrable (on ℝ³). If f has Schwartz decay and f > 0, then (1+‖v‖)^K * f(v) is integrable.