Arbitrary representatives for the periodized covariance

The canonical lift of a quotient point need not equal the Euclidean point used to define it. This file records that the two representatives differ by an integer period vector and transports representative independence of the covariance periodization across that equality.

theorem Anderson4D.SmoothCutoff.exists_periodVector_torusLift_periodizeR4 (x : R4) : ∃ (a : Z4), torusLift (periodizeR4 x) = x + covariancePeriodVector a

The canonical lift of an arbitrary Euclidean point modulo 2π differs from that point by an integer period vector.

theorem Anderson4D.SmoothCutoff.etaEpsT4_periodizeR4_eq_etaPeriodizationR4 (ρ : SmoothCutoff) (ε : ℝ) (x : R4) : ρ.etaEpsT4 ε (periodizeR4 x) = ρ.etaPeriodizationR4 ε x

Evaluating the torus covariance at the quotient of any Euclidean representative agrees with periodization based at that representative.

theorem Anderson4D.SmoothCutoff.etaPeriodizationR4_update_add_two_pi (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (i : Fin dim) (t : ℝ) : ρ.etaPeriodizationR4 ε (Function.update x i (t + 2 * Real.pi)) = ρ.etaPeriodizationR4 ε (Function.update x i t)

The arbitrary-representative periodization is 2π-periodic in each Euclidean coordinate.