OAI/Dynamics/SmoothObstruction/OrthogonalCocycle.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothObstruction.QR.continuous_gramSchmidt line 17

   Source documentation

   Continuity of the actual Gram--Schmidt algorithm on independent lists.

   theorem continuous_gramSchmidt (f : X → Fin d → E) (hf : Continuous f)
       (hind : ∀ x,LinearIndependent ℝ (f x)) (j : Fin d) :
       Continuous (fun x => gramSchmidt ℝ (f x) j) := by
   …

2. theorem OAI.SmoothObstruction.QR.continuous_gramSchmidtNormed line 38
3. abbrev OAI.SmoothObstruction.QR.Frame line 54

   Source documentation

   Finite orthonormal frames; the zero-dimensional case is included.

   abbrev Frame (d : ℕ) := {f : Fin d → EuclideanSpace ℝ (Fin d) // Orthonormal ℝ f}

4. instance OAI.SmoothObstruction.QR.(instance at line 56) line 56
5. instance OAI.SmoothObstruction.QR.(instance at line 59) line 59
6. def OAI.SmoothObstruction.QR.step line 75

   Source documentation

   The QR frame of the image of an orthonormal frame under an invertible map.

   noncomputable def step (A : EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d))
       (e : Frame d) : Frame d :=
   …

   Mentions: OAI.SmoothObstruction.QR.Frame

7. lemma OAI.SmoothObstruction.QR.continuous_step line 80
8. lemma OAI.SmoothObstruction.QR.inner_gramSchmidt_self line 98
9. lemma OAI.SmoothObstruction.QR.positive_diagonal line 110
10. def OAI.SmoothObstruction.QR.triangular line 118
11. lemma OAI.SmoothObstruction.QR.diagonal_pos line 122
12. lemma OAI.SmoothObstruction.QR.triangular_upper line 127
13. def OAI.SmoothObstruction.QR.basis line 151
14. lemma OAI.SmoothObstruction.QR.basis_apply line 154
15. lemma OAI.SmoothObstruction.QR.qr_factor line 160
16. def OAI.SmoothObstruction.QR.skew line 168
17. lemma OAI.SmoothObstruction.QR.continuous_skew line 173
18. theorem OAI.SmoothObstruction.QR.exists_stationary_qr line 181

    Source documentation

    The QR frame process carries a stationary law whose base marginal is exactly the given measure. The lift is constructed, not hypothesized.

    theorem exists_stationary_qr (T : X → X) (hT : Continuous T)
        (A : X → EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d))
        (hA : Continuous (fun x => (A x : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))))
        (μ : ProbabilityMeasure X) (hμ : MeasurePreserving T (μ : Measure X) (μ : Measure X)) :
        ∃ ν : ProbabilityMeasure (X × Frame d),
          MeasurePreserving (skew T A) (ν : Measure (X × Frame d)) (ν : Measure (X × Frame d)) ∧
          (ν : Measure (X × Frame d)).map Prod.fst=(μ : Measure X) := by
    …

    Mentions: OAI.SmoothObstruction.QR.Frame, OAI.SmoothObstruction.QR.skew

19. lemma OAI.SmoothObstruction.QR.continuous_diagonal line 194
20. lemma OAI.SmoothObstruction.QR.continuous_log_diagonal line 203
21. abbrev OAI.SmoothObstruction.OrbitCocycle.Path line 215
22. def OAI.SmoothObstruction.OrbitCocycle.code line 217
23. def OAI.SmoothObstruction.OrbitCocycle.shift line 220
24. lemma OAI.SmoothObstruction.OrbitCocycle.continuous_shift line 224
25. lemma OAI.SmoothObstruction.OrbitCocycle.measurable_code line 230
26. lemma OAI.SmoothObstruction.OrbitCocycle.code_shift line 237
27. theorem OAI.SmoothObstruction.OrbitCocycle.stationary_code line 245

    Source documentation

    Coding even a merely measurable bounded cocycle produces a genuine stationary law on a compact path space.

    theorem stationary_code (S : X ≃ₜ X) (A : X → CompactMatrix.Alphabet d K)
        (hA : Measurable A) (μ : ProbabilityMeasure X)
        (hS : MeasurePreserving S (μ : Measure X) (μ : Measure X)) :
        MeasurePreserving shift ((μ : Measure X).map (code S A))
          ((μ : Measure X).map (code S A)) := by
    …

    Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.OrbitCocycle.shift, OAI.SmoothObstruction.OrbitCocycle.code

28. def OAI.SmoothObstruction.OrbitCocycle.Actual line 267

    Source documentation

    This Borel set remembers the entire genuine orbit, and the actual cocycle value at every integer index, despite measurable trivializations.

    def Actual (S : X ≃ₜ X) (A : X → CompactMatrix.Alphabet d K) :
        Set (Path (X:=X) (d:=d) (K:=K)) := {p | p=code S A (p 0).1}

    Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.OrbitCocycle.code

29. lemma OAI.SmoothObstruction.OrbitCocycle.actual_measurable line 270
30. lemma OAI.SmoothObstruction.OrbitCocycle.code_actual line 282
31. def OAI.SmoothObstruction.OrbitCocycle.matrix line 285
32. lemma OAI.SmoothObstruction.OrbitCocycle.continuous_matrix line 288
33. theorem OAI.SmoothObstruction.OrbitCocycle.stationary_qr_code line 294

    Source documentation

    A stationary QR process for the genuine measurable cocycle. The path law, its original marginal, and concentration on actual orbits are proved.

    theorem stationary_qr_code (S : X ≃ₜ X) (A : X → CompactMatrix.Alphabet d K)
        (hA : Measurable A) (μ : ProbabilityMeasure X)
        (hS : MeasurePreserving S (μ : Measure X) (μ : Measure X)) :
        ∃ ν : ProbabilityMeasure (Path (X:=X) (d:=d) (K:=K) × QR.Frame d),
    …

    Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.QR.Frame

34. lemma OAI.SmoothObstruction.OrbitCocycle.preserving_pow line 315
35. lemma OAI.SmoothObstruction.OrbitCocycle.marginal_at line 325

    Source documentation

    Every deterministic-time observation has exactly the original base law.

    lemma marginal_at (S : X ≃ₜ X) (A : X → CompactMatrix.Alphabet d K)
        (hA : Measurable A) (μ : ProbabilityMeasure X)
        (hS : MeasurePreserving S (μ : Measure X) (μ : Measure X))
        (ν : ProbabilityMeasure (Path (X:=X) (d:=d) (K:=K) × QR.Frame d))
    …

    Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.QR.Frame