OAI/Dynamics/ThreeTorus/PhysicalBasis.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThreeTorus.PhysicalL2 line 14
2. def OAI.ThreeTorus.physicalIntegral line 16
3. lemma OAI.ThreeTorus.physicalIntegral_apply line 17
4. def OAI.ThreeTorus.physicalMeanZero line 24
5. lemma OAI.ThreeTorus.mem_physicalMeanZero line 25
6. lemma OAI.ThreeTorus.physicalMeanZero_closed line 28
7. def OAI.ThreeTorus.physicalCenter line 30
8. lemma OAI.ThreeTorus.continuous_physicalCenter line 32
9. lemma OAI.ThreeTorus.physicalCenter_ae line 34
10. lemma OAI.ThreeTorus.physicalCenter_mem line 40
11. lemma OAI.ThreeTorus.physicalCenter_eq_self line 44
12. def OAI.ThreeTorus.continuousCenter line 48
13. lemma OAI.ThreeTorus.continuousCenter_centered line 50
14. lemma OAI.ThreeTorus.toLp_continuousCenter line 55
15. lemma OAI.ThreeTorus.physical_real_closed line 68
16. instance OAI.ThreeTorus.PhysicalTest.(instance at line 86) line 86
17. instance OAI.ThreeTorus.PhysicalTest.(instance at line 87) line 87
18. instance OAI.ThreeTorus.PhysicalTest.(instance at line 89) line 89
19. lemma OAI.ThreeTorus.PhysicalTest.vec_eq_toLp line 91
20. lemma OAI.ThreeTorus.PhysicalTest.continuous_vec line 94
21. lemma OAI.ThreeTorus.PhysicalTest.vec_centered line 100
22. def OAI.ThreeTorus.SmoothDynamics.homeo line 117
23. def OAI.ThreeTorus.SmoothDynamics.orbit line 125
24. lemma OAI.ThreeTorus.SmoothDynamics.orbit_ae line 127
25. lemma OAI.ThreeTorus.SmoothDynamics.orbit_centered line 129
26. def OAI.ThreeTorus.SmoothDynamics.laurent line 135
27. lemma OAI.ThreeTorus.SmoothDynamics.laurent_mem_span line 136
28. lemma OAI.ThreeTorus.SmoothDynamics.tendsto_orbit line 141
29. lemma OAI.ThreeTorus.SmoothDynamics.tendsto_laurent line 146
30. theorem OAI.ThreeTorus.exists_physical_limit line 156

    Source documentation

    The diagonal produces an actual real centered vector and exact bilateral orthonormality, while retaining EVERY earlier polynomial in the same limit map.

    theorem exists_physical_limit (test : ℕ → PhysicalTest) (e : ℕ → ℝ)
        (he : ∀ n, 0 < e n) :
        ∃ D : SmoothDynamics, ∃ f : PhysicalL2,
          f ∈ physicalMeanZero ∧ (∀ᵐ x ∂tripleVolume, (f x).im=0) ∧
          Orthonormal ℂ (D.orbit f) ∧
          ∃ c : ℕ → (ℤ →₀ ℂ), ∀ i, dist (test i).vec (D.laurent f (c i)) ≤ e i := by
    …

    Mentions: OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.SmoothDynamics, OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.physicalMeanZero, OAI.ThreeTorus.tripleVolume

31. lemma OAI.ThreeTorus.continuous_real_mem_of_tests line 204

    Source documentation

    Every real centered continuous vector belongs to the linear span of the bounded physical tests, with its actual normalization scalar.

    lemma continuous_real_mem_of_tests (K : Submodule ℂ PhysicalL2)
        (hK : ∀ h : PhysicalTest, h.vec ∈ K)
        (g : C(TripleTorus,ℂ)) (hg : ∀ x, conj (g x)=g x)
        (hgc : ∫ x, g x ∂tripleVolume=0) : ContinuousMap.toLp 2 tripleVolume ℂ g ∈ K := by
    …

    Mentions: OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume

32. lemma OAI.ThreeTorus.continuous_centered_mem_of_tests line 232
33. lemma OAI.ThreeTorus.physical_tests_total line 265

    Source documentation

    Bounded real tests exhaust the FULL complex centered L2 space, not just a real or cyclic subspace.

    lemma physical_tests_total (K : Submodule ℂ PhysicalL2) (hclosed : IsClosed (K : Set PhysicalL2))
        (hK : ∀ h : PhysicalTest, h.vec ∈ K) {f : PhysicalL2} (hf : f ∈ physicalMeanZero) : f ∈ K := by
    …

    Mentions: OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.physicalMeanZero

34. theorem OAI.ThreeTorus.exists_total_physical_tests line 278

    Source documentation

    A single honest countable family of real bounded centered continuous tests suffices. Its full complex span is dense after closure.

    theorem exists_total_physical_tests : ∃ test : ℕ → PhysicalTest,
        ∀ K : Submodule ℂ PhysicalL2, IsClosed (K : Set PhysicalL2) →
          (∀ n, (test n).vec ∈ K) → ∀ f ∈ physicalMeanZero, f ∈ K := by
    …

    Mentions: OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.physicalMeanZero

35. theorem OAI.ThreeTorus.exists_physical_basis line 299

    Source documentation

    Unconditional geometric spectral basis on the physical product torus. The closure here is exactly the FULL complex kernel of the volume integral.

    theorem exists_physical_basis : ∃ D : SmoothDynamics, ∃ f : PhysicalL2,
        f ∈ physicalMeanZero ∧ (∀ᵐ x ∂tripleVolume, (f x).im=0) ∧
        Orthonormal ℂ (D.orbit f) ∧
        (Submodule.span ℂ (Set.range (D.orbit f))).topologicalClosure=physicalMeanZero := by
    …

    Mentions: OAI.ThreeTorus.SmoothDynamics, OAI.ThreeTorus.PhysicalL2, OAI.ThreeTorus.physicalMeanZero, OAI.ThreeTorus.tripleVolume