Documentation

Mathlib.MeasureTheory.MeasurableSpace.Invariants

σ-algebra of sets invariant under a self-map #

In this file we define MeasurableSpace.invariants (f : α → α) to be the σ-algebra of sets s : Set α such that

def MeasurableSpace.invariants {α : Type u_1} [m : MeasurableSpace α] (f : αα) :

Given a self-map f : α → α, invariants f is the σ-algebra of measurable sets that are invariant under f.

A set s is (invariants f)-measurable iff it is meaurable w.r.t. the canonical σ-algebra on α and f ⁻¹' s = s.

Equations
Instances For
    theorem MeasurableSpace.measurableSet_invariants {α : Type u_1} [MeasurableSpace α] {f : αα} {s : Set α} :

    A set s is (invariants f)-measurable iff it is meaurable w.r.t. the canonical σ-algebra on α and f ⁻¹' s = s.

    theorem MeasurableSpace.measurable_invariants_dom {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {f : αα} {g : αβ} :
    Measurable g Measurable g ∀ (s : Set β), MeasurableSet sg f ⁻¹' s = g ⁻¹' s
    theorem MeasurableSpace.measurable_invariants_of_semiconj {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {fa : αα} {fb : ββ} {g : αβ} (hg : Measurable g) (hfg : Function.Semiconj g fa fb) :