σ-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
sis measurable w.r.t. the canonical σ-algebra onα;- and
f ⁻ˢ' s = s.
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
- MeasurableSpace.invariants f = { MeasurableSet' := fun (s : Set α) => MeasurableSet s ∧ f ⁻¹' s = s, measurableSet_empty := ⋯, measurableSet_compl := ⋯, measurableSet_iUnion := ⋯ }
Instances For
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 meaurable w.r.t. the canonical σ-algebra on α and f ⁻¹' s = s.
@[simp]
theorem
MeasurableSpace.invariants_id
{α : Type u_1}
[MeasurableSpace α]
:
MeasurableSpace.invariants id = inst✝
theorem
MeasurableSpace.invariants_le
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
:
MeasurableSpace.invariants f ≤ inst✝
theorem
MeasurableSpace.le_invariants_iterate
{α : Type u_1}
[MeasurableSpace α]
(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)
: