SpectralTransport.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

Measure-preserving torus transport, full mean-zero L2 isometry, ergodicity, and full circle spectral representation.

def OAI.ThreeTorus.SmoothDynamics.torusMap line 17
Source documentation
The produced physical action in the fixed torus coordinate convention.
```
def torusMap (k : ℤ) : Equiv.Perm Torus :=
…
```
Mentions: OAI.ThreeTorus.Torus
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_apply line 19
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_zero line 21
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_add line 24
def OAI.ThreeTorus.SmoothDynamics.torusAction line 28
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_zpow line 33
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_inv line 36
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_symm line 39
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_mp line 41
lemma OAI.ThreeTorus.SmoothDynamics.torusMap_smooth line 45
def OAI.ThreeTorus.physicalToTorus line 68
Source documentation
The coordinate change is a genuine isometry on the full L2 spaces.
```
def physicalToTorus : PhysicalL2 →ₗᵢ[ℂ] H :=
…
```
Mentions: OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.H
def OAI.ThreeTorus.torusToPhysical line 70
lemma OAI.ThreeTorus.physicalToTorus_ae line 73
lemma OAI.ThreeTorus.torusToPhysical_ae line 75
lemma OAI.ThreeTorus.physicalToTorus_torusToPhysical line 78
lemma OAI.ThreeTorus.torusToPhysical_physicalToTorus line 83
lemma OAI.ThreeTorus.physicalToTorus_centered_iff line 90
lemma OAI.ThreeTorus.torusToPhysical_centered_iff line 94
def OAI.ThreeTorus.physicalZeroToTorus line 97
lemma OAI.ThreeTorus.physicalZeroToTorus_surjective line 102
def OAI.ThreeTorus.physicalZeroEquiv line 106
lemma OAI.ThreeTorus.physical_subtype_dense line 111
Source documentation
Ambient closure equal to the centered kernel gives density in its actual subspace topology, not merely in some smaller abstract copy.
```
lemma physical_subtype_dense (v : ℤ → physicalMeanZero)
    (h : (Submodule.span ℂ (Set.range (fun n => (v n : PhysicalL2)))).topologicalClosure=physicalMeanZero) :
    Dense (Submodule.span ℂ (Set.range v) : Set physicalMeanZero) := by
…
```
Mentions: OAI.ThreeTorus.physicalMeanZero, OAI.ThreeTorus.PhysicalL2
lemma OAI.ThreeTorus.physicalZeroEquiv_dense_span line 129
lemma OAI.ThreeTorus.integral_eq_inner_one line 155
lemma OAI.ThreeTorus.meanZero_closed line 162
instance OAI.ThreeTorus.(instance at line 167) line 167
lemma OAI.ThreeTorus.integral_comp_preserving line 170
def OAI.ThreeTorus.koopman line 178
Source documentation
The actual Koopman operator, restricted to the full centered subspace.
```
def koopman {T : Torus → Torus} (hT : MeasurePreserving T μ μ) : H₀ →ₗᵢ[ℂ] H₀ where
…
```
Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.μ, OAI.ThreeTorus.H₀
lemma OAI.ThreeTorus.koopman_ae line 187
lemma OAI.ThreeTorus.koopman_orbit_step line 191
def OAI.ThreeTorus.circleMul line 202
Source documentation
Circle coordinate multiplication, constructed on L² representatives.
```
def circleMul (n : ℤ) (f : CircleH) : CircleH :=
…
```
Mentions: OAI.ThreeTorus.CircleH
lemma OAI.ThreeTorus.circleMul_ae line 209
def OAI.ThreeTorus.circleMulLI line 213
lemma OAI.ThreeTorus.circleMul_fourier line 237

lemma OAI.ThreeTorus.spectral_model_of_basis line 247

Source documentation

The bilateral full-space basis determines the stated circle unitary. This is the spectral-model completion step only, not existence of the basis.

lemma spectral_model_of_basis {T : Equiv.Perm Torus} (hT : MeasurePreserving T μ μ)
    {f : H₀} {v : ℤ → H₀}
    (hv : ∀ n : ℤ, ∀ᵐ x ∂μ, (v n).1 x = f.1 ((T^n) x))
    (ho : Orthonormal ℂ v) (hd : Dense (Submodule.span ℂ (Set.range v) : Set H₀)) :
    ∃ W : H₀ ≃ₗᵢ[ℂ] CircleH,
      (∀ n : ℤ, W (v n) = fourierLp 2 n) ∧
      ∀ g : H₀, ∃ h : H₀,
        (∀ᵐ x ∂μ, h.1 x = g.1 (T x)) ∧
        (∀ᵐ z ∂AddCircle.haarAddCircle, W h z = fourier 1 z * W g z) := by
…

Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.μ, OAI.ThreeTorus.H₀, OAI.ThreeTorus.CircleH

lemma OAI.ThreeTorus.circleMul_one_fixed line 282
Source documentation
Multiplication by the circle coordinate has no nonzero fixed vector.
```
lemma circleMul_one_fixed {g : CircleH} (hg : circleMulLI 1 g = g) : g = 0 := by
…
```
Mentions: OAI.ThreeTorus.CircleH, OAI.ThreeTorus.circleMulLI

lemma OAI.ThreeTorus.koopman_no_fixed_of_basis line 312

Source documentation

The circle model excludes invariant vectors in the full centered space.

lemma koopman_no_fixed_of_basis {T : Equiv.Perm Torus} (hT : MeasurePreserving T μ μ)
    {f : H₀} {v : ℤ → H₀}
    (hv : ∀ n : ℤ, ∀ᵐ x ∂μ, (v n).1 x = f.1 ((T^n) x))
    (ho : Orthonormal ℂ v) (hd : Dense (Submodule.span ℂ (Set.range v) : Set H₀))
    {g : H₀} (hg : koopman hT g = g) : g = 0 := by
…

Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.μ, OAI.ThreeTorus.H₀, OAI.ThreeTorus.koopman

lemma OAI.ThreeTorus.ergodic_of_no_meanZero_fixed line 332
Source documentation
Invariant measurable sets give centered L² fixed vectors. This establishes ergodicity from the full mean-zero space, not from a proper cyclic subspace.
```
lemma ergodic_of_no_meanZero_fixed {T : Torus → Torus} (hT : MeasurePreserving T μ μ)
    (hfixed : ∀ g : H₀, koopman hT g = g → g = 0) : Ergodic T μ := by
…
```
Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.μ, OAI.ThreeTorus.H₀, OAI.ThreeTorus.koopman
lemma OAI.ThreeTorus.ergodic_of_basis line 379
lemma OAI.ThreeTorus.mainConclusion_of_basis line 388
Source documentation
Once the unconditional geometric construction produces its bilateral basis, all stated spectral and ergodic consequences follow. This lemma is not the existence theorem.
```
lemma mainConclusion_of_basis (T : Equiv.Perm Torus)
    (hs : Smooth T) (hsi : Smooth T.symm) (hT : MeasurePreserving T μ μ)
    (f : H₀) (hf : IsReal f) (v : ℤ → H₀)
    (hv : ∀ n : ℤ, ∀ᵐ x ∂μ, (v n).1 x = f.1 ((T^n) x))
    (ho : Orthonormal ℂ v) (hd : Dense (Submodule.span ℂ (Set.range v) : Set H₀)) :
    MainConclusion := by
…
```
Mentions: OAI.ThreeTorus.Torus, OAI.ThreeTorus.Smooth, OAI.ThreeTorus.μ, OAI.ThreeTorus.H₀, OAI.ThreeTorus.IsReal, OAI.ThreeTorus.MainConclusion