Quasi Measure Preserving Functions #
A map f : α → β is said to be quasi measure preserving (a.k.a. non-singular) w.r.t. measures
μa and μb if it is measurable and μb s = 0 implies μa (f ⁻¹' s) = 0.
That last condition can also be written μa.map f ≪ μb (the map of μa by f is
absolutely continuous with respect to μb).
Main definitions #
MeasureTheory.Measure.QuasiMeasurePreserving f μa μb:fis quasi measure preserving with respect toμaandμb.
structure
MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m0 : MeasurableSpace α}
(f : α → β)
(μa : MeasureTheory.Measure α := by volume_tac)
(μb : MeasureTheory.Measure β := by volume_tac)
:
A map f : α → β is said to be quasi measure preserving (a.k.a. non-singular) w.r.t. measures
μa and μb if it is measurable and μb s = 0 implies μa (f ⁻¹' s) = 0.
- measurable : Measurable f
- absolutelyContinuous : (MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb
Instances For
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.id
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
theorem
Measurable.quasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{f : α → β}
{_m0 : MeasurableSpace α}
(hf : Measurable f)
(μ : MeasureTheory.Measure α)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa μa' : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(ha : μa'.AbsolutelyContinuous μa)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb μb' : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(ha : μb.AbsolutelyContinuous μb')
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa μa' : MeasureTheory.Measure α}
{μb μb' : MeasureTheory.Measure β}
{f : α → β}
(ha : μa'.AbsolutelyContinuous μa)
(hb : μb.AbsolutelyContinuous μb')
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ}
{g : β → γ}
{f : α → β}
(hg : MeasureTheory.Measure.QuasiMeasurePreserving g μb μc)
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
MeasureTheory.Measure.QuasiMeasurePreserving (g ∘ f) μa μc
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.iterate
{α : Type u_1}
{mα : MeasurableSpace α}
{μa : MeasureTheory.Measure α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μa)
(n : ℕ)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
AEMeasurable f μa
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{R : Type u_5}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(c : R)
:
MeasureTheory.Measure.QuasiMeasurePreserving f (c • μa) (c • μb)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
Filter.Tendsto f (MeasureTheory.ae μa) (MeasureTheory.ae μb)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
{p : β → Prop}
(hg : ∀ᵐ (x : β) ∂μb, p x)
:
∀ᵐ (x : α) ∂μa, p (f x)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
{g₁ g₂ : β → δ}
(hg : g₁ =ᵐ[μb] g₂)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
{s : Set β}
(hs : μb s = 0)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{s t : Set β}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(h : s ≤ᵐ[μb] t)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{s t : Set β}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(h : s =ᵐ[μb] t)
:
theorem
MeasureTheory.NullMeasurableSet.preimage
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{s : Set β}
(hs : MeasureTheory.NullMeasurableSet s μb)
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
MeasureTheory.NullMeasurableSet (f ⁻¹' s) μa
The preimage of a null measurable set under a (quasi) measure preserving map is a null measurable set.
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(k : ℕ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{e : α ≃ α}
(he : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e) μ μ)
(he' : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) μ μ)
(k : ℤ)
(hs : ⇑e '' s =ᵐ[μ] s)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
Filter.limsup (fun (n : ℕ) => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
Filter.liminf (fun (n : ℕ) => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : f ⁻¹' s =ᵐ[μ] s)
:
For a quasi measure preserving self-map f, if a null measurable set s is a.e. invariant,
then it is a.e. equal to a measurable invariant set.
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq
{G : Type u_5}
{α : Type u_6}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(g : G)
(h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g⁻¹ • x) μ μ)
(h_ae_eq : s =ᵐ[μ] t)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq
{G : Type u_5}
{α : Type u_6}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(g : G)
(h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => -g +ᵥ x) μ μ)
(h_ae_eq : s =ᵐ[μ] t)
:
theorem
MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one
{G : Type u_5}
{α : Type u_6}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s)
(h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g • x) μ μ)
:
Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun (g : G) => g • s)
theorem
MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero
{G : Type u_5}
{α : Type u_6}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s)
(h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ)
:
Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun (g : G) => g +ᵥ s)
theorem
MeasureTheory.NullMeasurableSet.mono_ac
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.NullMeasurableSet s μ)
(hle : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.NullMeasurableSet.mono
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.NullMeasurableSet s μ)
(hle : ν ≤ μ)
:
theorem
MeasureTheory.AEDisjoint.preimage
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → β}
{s t : Set β}
(ht : MeasureTheory.AEDisjoint ν s t)
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν)
:
MeasureTheory.AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)
theorem
MeasurableEquiv.quasiMeasurePreserving_symm
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ