Torus Integration Lemmas

Box integral machinery, integration by parts on T³, curl integral vanishing, and the energy method proof that harmonic functions on T³ are constant.

def box3 : Set (Fin 3 → ℝ)

The half-open unit box (0, 1]³ ⊆ ℝ³, a fundamental domain for T³ = (ℝ/ℤ)³.

Equations

• box3 = Set.univ.pi fun (x : Fin 3) => Set.Ioc 0 1

theorem measure_torus_eq_map : MeasureTheory.volume = MeasureTheory.Measure.map torusMk (MeasureTheory.volume.restrict box3)

The volume measure on T³ is the pushforward of the box measure.

theorem integral_torus_eq_integral_box (g : Torus3 → ℝ) (hg : Continuous g) : ∫ (x : Torus3), g x = ∫ (y : Fin 3 → ℝ) in box3, g (torusMk y)

∫ over T³ = ∫ over [0,1]³ of the periodic lift.

theorem integral_derivative_periodic_zero (F : (Fin 3 → ℝ) → ℝ) (i : Fin 3) (hF : ContDiff ℝ 1 F) (hper : ∀ (x : Fin 3 → ℝ), F (x + Pi.single i 1) = F x) : ∫ (y : Fin 3 → ℝ) in box3, (fderiv ℝ F y) (Pi.single i 1) = 0

∫ ∂F/∂xᵢ over [0,1]³ = 0 for periodic F (FTC + periodicity).

theorem torus_gradX_integral_zero (f : Torus3 → ℝ) (i : Fin 3) (hf : ContDiff ℝ 1 (periodicLift f)) : ∫ (x : Torus3), torusGradX f x i = 0

∫ torusGradX f x i = 0 on T³ (FTC + periodicity on the box). Proved by Aristotle.

theorem torusGradX_mul (φ ψ : Torus3 → ℝ) (i : Fin 3) (hφ : Differentiable ℝ (periodicLift φ)) (hψ : Differentiable ℝ (periodicLift ψ)) (x : Torus3) : torusGradX (fun (z : Torus3) => φ z * ψ z) x i = φ x * torusGradX ψ x i + ψ x * torusGradX φ x i

Product rule: ∂(φψ)/∂xᵢ = φ · ∂ψ/∂xᵢ + ψ · ∂φ/∂xᵢ. Proved by Aristotle.

theorem torus_hIBP_spatial (φ ψ : Torus3 → ℝ) (i : Fin 3) (hφ : ContDiff ℝ 1 (periodicLift φ)) (hψ : ContDiff ℝ 1 (periodicLift ψ)) : ∫ (x : Torus3), φ x * torusGradX ψ x i = -∫ (x : Torus3), ψ x * torusGradX φ x i

IBP on T³: ∫ φ · ∂ψ/∂xᵢ = -∫ ψ · ∂φ/∂xᵢ. Proved by Aristotle.

theorem torus_hCurlIntZero (F : Torus3 → Fin 3 → ℝ) (u : Fin 3 → ℝ) (hF_diff : ∀ (j : Fin 3), ContDiff ℝ 1 (periodicLift fun (x : Torus3) => F x j)) : ∫ (x : Torus3), u ⬝ᵥ torusCurlX F x = 0

∫ u · (∇×F) = 0 on T³. Each gradient integral vanishes by periodicity.

theorem torus_hHarmonic_const (φ : Torus3 → ℝ) (hd : ContDiff ℝ 2 (periodicLift φ)) (hharmonic : ∀ (x : Torus3), torusDivX (torusGradX φ) x = 0) (x y : Torus3) : φ x = φ y

Harmonic → constant on T³. Energy method using IBP.