σ-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

• s is measurable w.r.t. the canonical σ-algebra on α;
• and f ⁻¹' s = s.

@[instance_reducible]

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

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 measurable w.r.t. the canonical σ-algebra on α and f ⁻¹' s = s.

Equations

• MeasurableSpace.invariants f = { MeasurableSet' := fun (s : Set α) => MeasurableSet s ∧ f ⁻¹' s = s, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }

theorem MeasurableSpace.measurableSet_invariants {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} : MeasurableSet s ↔ MeasurableSet s ∧ f ⁻¹' s = s

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

@[simp]

theorem MeasurableSpace.invariants_id {α : Type u_1} [MeasurableSpace α] : invariants id = inst✝

theorem MeasurableSpace.invariants_le {α : Type u_1} [MeasurableSpace α] (f : α → α) : invariants f ≤ inst✝

theorem MeasurableSpace.inf_le_invariants_comp {α : Type u_1} [MeasurableSpace α] (f g : α → α) : invariants f ⊓ invariants g ≤ invariants (f ∘ g)

theorem MeasurableSpace.le_invariants_iterate {α : Type u_1} [MeasurableSpace α] (f : α → α) (n : ℕ) : invariants f ≤ invariants f^[n]

theorem MeasurableSpace.measurable_invariants_dom {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {f : α → α} {g : α → β} : Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ 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) : Measurable g

theorem MeasurableSpace.comp_eq_of_measurable_invariants {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {f : α → α} {g : α → β} [MeasurableSingletonClass β] (h : Measurable g) : g ∘ f = g