Torus Type Definitions and Differential Operators

Defines the 3-torus T^3 = (R/Z)^3, the projection torusMk, the periodic lift, and differential operators (torusGradX, torusDivX, torusCurlX) via the periodic lift. The FlatTorus3 instance is assembled in TorusInstance.lean.

@[reducible, inline]

abbrev Torus3 : Type

The 3-torus: product of three circles with period 1.

Equations

• Torus3 = (Fin 3 → AddCircle 1)

instance instFactLtRealOfNat_aristotle : Fact (0 < 1)

instance instCompactSpaceTorus3 : CompactSpace Torus3

instance instT2SpaceTorus3 : T2Space Torus3

instance instIsFiniteMeasureTorus3Volume : MeasureTheory.IsFiniteMeasure MeasureTheory.volume

instance instSigmaFiniteTorus3Volume : MeasureTheory.SigmaFinite MeasureTheory.volume

def torusMk (x : Fin 3 → ℝ) : Torus3

The quotient map ℝ³ → T³, sending each coordinate to its equivalence class.

Equations

• torusMk x i = ↑(x i)

theorem torusMk_surjective : Function.Surjective torusMk

def periodicLift (f : Torus3 → ℝ) : (Fin 3 → ℝ) → ℝ

The periodic lift of a function on the torus to ℝ³.

Equations

• periodicLift f = f ∘ torusMk

theorem periodicLift_periodic (f : Torus3 → ℝ) (x : Fin 3 → ℝ) (i : Fin 3) : periodicLift f (x + Pi.single i 1) = periodicLift f x

theorem periodicLift_shift (f : Torus3 → ℝ) (x y : Fin 3 → ℝ) (h : torusMk x = torusMk y) (z : Fin 3 → ℝ) : periodicLift f (z + (x - y)) = periodicLift f z

The periodic lift at shifted argument equals the original when the shift maps to the same torus point.

theorem periodicLift_fderiv_eq (f : Torus3 → ℝ) (x y : Fin 3 → ℝ) (h : torusMk x = torusMk y) : fderiv ℝ (periodicLift f) x = fderiv ℝ (periodicLift f) y

fderiv of the lift at two points that map to the same torus point are equal. This follows because f̃(x) = f̃(x + n) for integer n, so the 1-jets agree.

def torusGradX (f : Torus3 → ℝ) (x : Torus3) : Fin 3 → ℝ

Spatial gradient on T³. For f : T³ → ℝ, we lift to ℝ³, compute fderiv, and read off components. This is well-defined by periodicLift_fderiv_eq.

Equations

• torusGradX f x = fun (i : Fin 3) => (fderiv ℝ (periodicLift f) ⋯.choose) (Pi.single i 1)

def torusDivX (F : Torus3 → Fin 3 → ℝ) (x : Torus3) : ℝ

Spatial divergence on T³.

Equations

• torusDivX F x = ∑ i : Fin 3, (fderiv ℝ (fun (y : Fin 3 → ℝ) => periodicLift (fun (z : Torus3) => F z i) y) ⋯.choose) (Pi.single i 1)

def torusCurlX (F : Torus3 → Fin 3 → ℝ) (x : Torus3) : Fin 3 → ℝ

Spatial curl on T³.

Equations

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

theorem periodicLift_torusGradX (φ : Torus3 → ℝ) (i : Fin 3) (y : Fin 3 → ℝ) : periodicLift (fun (z : Torus3) => torusGradX φ z i) y = (fderiv ℝ (periodicLift φ) y) (Pi.single i 1)

The periodic lift of the gradient component equals the fderiv of the lift. This resolves the choose ambiguity: at each point, the gradient uses a chosen preimage, but by periodicLift_fderiv_eq, the fderiv is the same for any preimage of the same torus point.

theorem fderiv_const_mul_always {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ) (g : E → ℝ) (x : E) : fderiv ℝ (fun (y : E) => c * g y) x = c • fderiv ℝ g x

fderiv(c * g) = c • fderiv(g) unconditionally. When g is differentiable: by fderiv_const_smul. When g is not differentiable and c ≠ 0: c * g is also not differentiable, so both sides are the zero map. When c = 0: both sides are 0.

theorem fderiv_exp_comp_always {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : E → ℝ) (x : E) : fderiv ℝ (fun (y : E) => Real.exp (g y)) x = Real.exp (g x) • fderiv ℝ g x

fderiv(exp ∘ g) x = exp(g x) • fderiv g x unconditionally. When g is differentiable: by fderiv_exp. When g is not differentiable: exp ∘ g is also not differentiable (since g = log ∘ exp ∘ g and log is smooth on (0,∞)), so both sides are 0.

theorem clairaut_fderiv {n : ℕ} (g : (Fin n → ℝ) → ℝ) (x : Fin n → ℝ) (i j : Fin n) (hg : ContDiff ℝ 2 g) : (fderiv ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ g y) (Pi.single j 1)) x) (Pi.single i 1) = (fderiv ℝ (fun (y : Fin n → ℝ) => (fderiv ℝ g y) (Pi.single i 1)) x) (Pi.single j 1)

Clairaut's theorem via fderiv: ∂²f/∂xᵢ∂xⱼ = ∂²f/∂xⱼ∂xᵢ for C² functions.

theorem torus_hGradConst (φ : Torus3 → ℝ) (hconst : ∀ (x y : Torus3), φ x = φ y) (x : Torus3) : torusGradX φ x = 0

hGradConst: gradient of constant function vanishes.

theorem torus_hGradAdd' (f g : Torus3 → ℝ) (hf : ContDiff ℝ 1 (periodicLift f)) (hg : ContDiff ℝ 1 (periodicLift g)) (x : Torus3) : torusGradX (fun (y : Torus3) => f y + g y) x = torusGradX f x + torusGradX g x

hGradAdd: gradient additivity for C¹ functions.

theorem torus_hSpatialVelocityFubini (F : Torus3 → (Fin 3 → ℝ) → ℝ) (hF_joint : MeasureTheory.Integrable (Function.uncurry F) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (x : Torus3) (v : Fin 3 → ℝ), F x v = ∫ (v : Fin 3 → ℝ) (x : Torus3), F x v

hSpatialVelocityFubini: swap spatial and velocity integrals. Uses SigmaFinite (from CompactSpace + IsFiniteMeasure).

theorem torus_hSpatialPos (g : Torus3 → ℝ) (hg_pos : ∀ (x : Torus3), 0 < g x) (hg_cont : Continuous g) : 0 < ∫ (x : Torus3), g x

hSpatialPos: positive function has positive integral.

theorem torus_hSpatialNonnegZero (g : Torus3 → ℝ) (hg_nn : ∀ (x : Torus3), 0 ≤ g x) (hg_int : ∫ (x : Torus3), g x = 0) (hg_cont : Continuous g) (x : Torus3) : g x = 0

hSpatialNonnegZero: nonneg function with zero integral is zero.

theorem isOpenQuotientMap_torusMk : IsOpenQuotientMap torusMk

torusMk is an open quotient map (product of open quotient maps).

theorem continuous_torusGradX (f : Torus3 → ℝ) (i : Fin 3) (hf : ContDiff ℝ 1 (periodicLift f)) : Continuous fun (x : Torus3) => torusGradX f x i

torusGradX is continuous (uses quotient map property).