OAI/MeasureTheory/CompactFactors/Stationary.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.StationaryMean.inner line 16
  2. lemma OAI.EuclideanFiveColor.StationaryMean.inner_norm line 20
  3. def OAI.EuclideanFiveColor.StationaryMean.outer line 22
  4. def OAI.EuclideanFiveColor.StationaryMean.average line 25
  5. lemma OAI.EuclideanFiveColor.StationaryMean.inner_add line 27
  6. lemma OAI.EuclideanFiveColor.StationaryMean.inner_smul line 29
  7. lemma OAI.EuclideanFiveColor.StationaryMean.outer_add line 31
  8. lemma OAI.EuclideanFiveColor.StationaryMean.outer_smul line 35
  9. lemma OAI.EuclideanFiveColor.StationaryMean.average_add line 38
  10. lemma OAI.EuclideanFiveColor.StationaryMean.average_smul line 40
  11. lemma OAI.EuclideanFiveColor.StationaryMean.average_mono line 42
  12. lemma OAI.EuclideanFiveColor.StationaryMean.average_const line 47
  13. lemma OAI.EuclideanFiveColor.StationaryMean.average_translation line 54
  14. lemma OAI.EuclideanFiveColor.StationaryMean.average_rotation line 67
  15. def OAI.EuclideanFiveColor.StationaryMean.functional line 80
  16. def OAI.EuclideanFiveColor.StationaryMean.measure line 85
  17. instance OAI.EuclideanFiveColor.StationaryMean.(instance at line 86) line 86
  18. instance OAI.EuclideanFiveColor.StationaryMean.(instance at line 87) line 87
  19. lemma OAI.EuclideanFiveColor.StationaryMean.integral line 88
  20. instance OAI.EuclideanFiveColor.StationaryMean.(instance at line 90) line 90
  21. lemma OAI.EuclideanFiveColor.StationaryMean.preserving_of_average line 97
  22. instance OAI.PlaneFiveColor.Spectral.K_countable line 112
  23. theorem OAI.PlaneFiveColor.Spectral.exists_terminal_factor line 126

    Source documentation

    An actual standard Borel factor with universal relative spectral singularity and an ergodic conditional square. Maximality is countable, inside the separable ambient L² space.

    theorem exists_terminal_factor (μ : Measure X) [IsProbabilityMeasure μ] [ErgodicSMul K X μ] :
    ∃ p : X → OrbitSpace K, ∃ hp : Measurable p,
      (∀ k : K, ∀ᵐ x ∂μ, p (k • x) = k • p x) ∧ UniversalGood μ p ∧
      ErgodicSMul K (X × X) (RelativeProduct.law μ p hp) := by
…

    Mentions: OAI.PlaneFiveColor.Spectral.K, OAI.PlaneFiveColor.Spectral.UniversalGood