σ-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
.
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.inf_le_invariants_comp
{α : Type u_1}
[MeasurableSpace α]
(f : α → α)
(g : α → α)
:
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)
: