CountableInvariantRepresentative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact representatives for countable invariant actions

For a countable group, one common conull invariant set makes all the almost-everywhere invariance identities simultaneous. Extending by zero on its complement gives a measurable function constant on every orbit.

theorem OAI.PolycyclicRecognition.measurable_invariantRepresentative line 24

Source documentation

A measurable almost invariant real function has an exactly invariant version.

theorem measurable_invariantRepresentative (f : X → ℝ) (hf : Measurable f)
    (hi : ∀ g : G, (fun x => f (g • x)) =ᵐ[μ] f) :
    ∃ F : X → ℝ, Measurable F ∧ F =ᵐ[μ] f ∧ ∀ (g : G) x, F (g • x) = F x := by
…

theorem OAI.PolycyclicRecognition.aemeasurable_invariantRepresentative line 53

Source documentation

The same construction starts from any almost-everywhere measurable function.

theorem aemeasurable_invariantRepresentative [SMulInvariantMeasure G X μ]
    (f : X → ℝ) (hf : AEMeasurable f μ)
    (hi : ∀ g : G, (fun x => f (g • x)) =ᵐ[μ] f) :
    ∃ F : X → ℝ, Measurable F ∧ F =ᵐ[μ] f ∧ ∀ (g : G) x, F (g • x) = F x := by
…