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

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

theorem MeasurableSpace.measurableSet_invariants {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} : Iff (MeasurableSet s) (And (MeasurableSet s) (Eq (Set.preimage f s) s))

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_id {α : Type u_1} [MeasurableSpace α] : Eq (invariants id) inst✝

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

theorem MeasurableSpace.inf_le_invariants_comp {α : Type u_1} [MeasurableSpace α] (f g : α → α) : LE.le (Min.min (invariants f) (invariants g)) (invariants (Function.comp f g))

theorem MeasurableSpace.le_invariants_iterate {α : Type u_1} [MeasurableSpace α] (f : α → α) (n : Nat) : LE.le (invariants f) (invariants (Nat.iterate f n))

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