set_option linter.style.longLine false

FlatTorus3 Instance for T^3

Proves the remaining FlatTorus3 axioms (Laplacian maximum principle, Killing implies harmonic, curl-div implies harmonic) and assembles the full FlatTorus3 instance on Fin 3 -> AddCircle 1.

theorem torus_hLaplacianMaxNonpos (φ : Torus3 → ℝ) (x₀ : Torus3) (hd : ContDiff ℝ 1 (periodicLift φ)) (hmax : ∀ (x : Torus3), φ x ≤ φ x₀) : torusDivX (torusGradX φ) x₀ ≤ 0

hLaplacianMaxNonpos: Δφ ≤ 0 at a global maximum. Second derivative test: at a maximum, the Hessian is negative semi-definite, so its trace (= Laplacian) ≤ 0.

theorem torus_hKillingToHarmonic (b : Torus3 → Fin 3 → ℝ) (hb_C1 : ∀ (j : Fin 3), ContDiff ℝ 1 (periodicLift fun (z : Torus3) => b z j)) (hb_C2 : ∀ (j i : Fin 3), ContDiff ℝ 1 (periodicLift fun (x : Torus3) => torusGradX (fun (y : Torus3) => b y j) x i)) (hKilling : ∀ (x : Torus3) (i j : Fin 3), torusGradX (fun (y : Torus3) => b y j) x i + torusGradX (fun (y : Torus3) => b y i) x j = 0) (j : Fin 3) (x : Torus3) : torusDivX (torusGradX fun (y : Torus3) => b y j) x = 0

theorem torus_hCurlZeroDivZeroHarmonic (F : Torus3 → Fin 3 → ℝ) (hF_C1 : ∀ (i : Fin 3), ContDiff ℝ 1 (periodicLift fun (z : Torus3) => F z i)) (hF_C2 : ∀ (i j : Fin 3), ContDiff ℝ 1 (periodicLift fun (x : Torus3) => torusGradX (fun (y : Torus3) => F y i) x j)) (hcurl : ∀ (x : Torus3), torusCurlX F x = 0) (hdiv : ∀ (x : Torus3), torusDivX F x = 0) (i : Fin 3) (x : Torus3) : torusDivX (torusGradX fun (y : Torus3) => F y i) x = 0

hCurlZeroDivZeroHarmonic: irrotational + solenoidal → harmonic on flat T³.

instance instFlatTorus3Torus3 : VML.FlatTorus3 Torus3

Equations

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