set_option linter.style.longLine false

Derived Lemmas for the FlatTorus3 Typeclass

Lemmas derived from the FlatTorus3 axioms: spatial multiplication, gradient vanishing, chain rules for log, integration by parts consequences, Laplacian sign at extrema, and Maxwellian parameter regularity.

theorem VML.FlatTorus3.IsSpatiallySmooth.of_le {X : Type u_1} [FlatTorus3 X] {n m : ℕ∞} {f : X → ℝ} (h : IsSpatiallySmooth n f) (hle : m ≤ n) : IsSpatiallySmooth m f

theorem VML.FlatTorus3.hSpatialMul {X : Type u_1} [FlatTorus3 X] (g : X → ℝ) (c : ℝ) : (spatialIntegral fun (x : X) => g x * c) = spatialIntegral g * c

Scalar multiplication: ∫ g(x) * c = (∫ g) * c. Proved from Mathlib's integral_mul_const.

theorem VML.FlatTorus3.hGradZeroConst {X : Type u_1} [FlatTorus3 X] (φ : X → ℝ) (hd : IsSpatiallySmooth 2 φ) (h : ∀ (x : X), gradX φ x = 0) (x y : X) : φ x = φ y

Zero gradient implies spatially constant (derived from hHarmonic_const + hDivLinear).

theorem VML.FlatTorus3.hGradChainLog {X : Type u_1} [FlatTorus3 X] (g : X → ℝ) (hg_diff : IsSpatiallySmooth 1 g) (hg : ∀ (x : X), 0 < g x) (x : X) (i : Fin 3) : gradX (fun (y : X) => Real.log (g y)) x i = 1 / g x * gradX g x i

Chain rule for log: gradX(log ∘ g) = (1/g) · gradX(g) when g > 0. Derived from hGradChainExp: gradX(exp(log g)) = g · gradX(log g) = gradX(g).

theorem VML.FlatTorus3.hGradIntZero {X : Type u_1} [FlatTorus3 X] (g : X → ℝ) (hg : IsSpatiallySmooth 1 g) (u : Fin 3 → ℝ) : ∫ (x : X), u ⬝ᵥ gradX g x = 0

Gradient integral vanishes (Stokes for 0-forms: ∫_M dg = 0). Derived from hIBP_spatial + hGradConst + hGradIntegrable.

theorem VML.FlatTorus3.hGradAddConst {X : Type u_1} [FlatTorus3 X] (f : X → ℝ) (hf : IsSpatiallySmooth 1 f) (c : ℝ) (x : X) : gradX (fun (y : X) => f y + c) x = gradX f x

Adding a constant doesn't change the gradient. Derived from hGradChainExp + hGradScalarMul via the exp trick: exp(f+c) = exp(c)*exp(f), so by the chain rule and scalar multiplication, exp(f(x)+c) * gradX(f+c)(x) = exp(c) * exp(f(x)) * gradX(f)(x). Cancelling exp(f(x)+c) > 0 gives gradX(f+c) = gradX(f).

theorem VML.FlatTorus3.hLaplacianMinNonneg {X : Type u_1} [FlatTorus3 X] (φ : X → ℝ) (hφ : IsSpatiallySmooth 2 φ) (x₀ : X) (hmin : ∀ (x : X), φ x₀ ≤ φ x) : 0 ≤ divX (gradX φ) x₀

Second derivative test: Laplacian ≥ 0 at a minimum. Derived from hLaplacianMaxNonpos applied to -φ, using linearity of grad and div.

theorem VML.FlatTorus3.maxwellian_params_isSpatiallySmooth {X : Type u_1} [FlatTorus3 X] {n : ℕ∞} (f : X → (Fin 3 → ℝ) → ℝ) (hf_pos : ∀ (x : X) (v : Fin 3 → ℝ), 0 < f x v) (hDiff_fv : ∀ (v : Fin 3 → ℝ), IsSpatiallySmooth n fun (x : X) => f x v) (a : X → ℝ) (b : X → Fin 3 → ℝ) (c : X → ℝ) (hform : ∀ (x : X) (v : Fin 3 → ℝ), f x v = Real.exp (a x + b x ⬝ᵥ v + c x * normSq v)) : IsSpatiallySmooth n a ∧ (∀ (j : Fin 3), IsSpatiallySmooth n fun (x : X) => b x j) ∧ IsSpatiallySmooth n c

Maxwellian regularity: if f(x,v) = exp(a(x) + b(x)·v + c(x)|v|²) with f > 0 and f(·,v) spatially differentiable for each v, then a, bⱼ, c are spatially differentiable.

Proof: Evaluate log f at v = 0, eⱼ, 2e₀ to extract the coefficients as linear combinations of the spatially differentiable functions x ↦ log f(x, v).