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
  • One or more equations did not get rendered due to their size.
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.invariants_le {α : Type u_1} [MeasurableSpace α] (f : αα) :
    LE.le (invariants f) inst✝
    theorem MeasurableSpace.measurable_invariants_dom {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {f : αα} {g : αβ} :
    Iff (Measurable g) (And (Measurable g) (∀ (s : Set β), MeasurableSet sEq (Set.preimage (Function.comp g f) s) (Set.preimage 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) :