InvariantL2Representative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed L2 vectors and orbit averaging for a countable action

This connects the Hilbert-space averaging theorem to measurable functions on the original probability space. Fixed vectors receive exactly invariant measurable representatives, rather than just invariant equivalence classes.

theorem OAI.PolycyclicRecognition.fixedL2_invariantRepresentative line 25

Source documentation

Simultaneous measurable representative of a fixed vector.

theorem fixedL2_invariantRepresentative (v : Lp ℝ 2 μ)
    (hfix : ∀ g : G, stationaryPullback μ g v = v) :
    ∃ F : X → ℝ, Measurable F ∧ F =ᵐ[μ] v ∧ ∀ (g : G) x, F (g • x) = F x := by
…

Mentions: OAI.PolycyclicRecognition.stationaryPullback

theorem OAI.PolycyclicRecognition.exists_L2_orbitAverage line 40

Source documentation

Convex orbit averaging produces an exactly invariant measurable limit.

theorem exists_L2_orbitAverage (v : Lp ℝ 2 μ) :
    ∃ (w : Lp ℝ 2 μ) (F : X → ℝ),
      w ∈ closure (convexHull ℝ (range (fun g : G => stationaryPullback μ g v))) ∧
      Measurable F ∧ F =ᵐ[μ] w ∧ ∀ (g : G) x, F (g • x) = F x := by
…

Mentions: OAI.PolycyclicRecognition.stationaryPullback