σ-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
- 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 α}
:
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_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)
: