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 : Measure α := by volume_tac)
(μb : 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 : (map f μa).AbsolutelyContinuous μb
Instances For
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.id
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : 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' : Measure α}
{μb : Measure β}
{f : α → β}
(h : QuasiMeasurePreserving f μa μb)
(ha : μa'.AbsolutelyContinuous μa)
:
QuasiMeasurePreserving f μa' μb
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb μb' : Measure β}
{f : α → β}
(h : QuasiMeasurePreserving f μa μb)
(ha : μb.AbsolutelyContinuous μb')
:
QuasiMeasurePreserving f μa μb'
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa μa' : Measure α}
{μb μb' : Measure β}
{f : α → β}
(ha : μa'.AbsolutelyContinuous μa)
(hb : μb.AbsolutelyContinuous μb')
(h : QuasiMeasurePreserving f μa μb)
:
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 : Measure α}
{μb : Measure β}
{μc : Measure γ}
{g : β → γ}
{f : α → β}
(hg : QuasiMeasurePreserving g μb μc)
(hf : QuasiMeasurePreserving f μa μb)
:
QuasiMeasurePreserving (g ∘ f) μa μc
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.iterate
{α : Type u_1}
{mα : MeasurableSpace α}
{μa : Measure α}
{f : α → α}
(hf : QuasiMeasurePreserving f μa μa)
(n : ℕ)
:
QuasiMeasurePreserving f^[n] μa μa
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : QuasiMeasurePreserving f μa μb)
:
AEMeasurable f μa
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(hf : QuasiMeasurePreserving f μa μb)
{f' : α → β}
(hf' : Measurable f')
(h : f =ᵐ[μa] f')
:
QuasiMeasurePreserving f' μa μb
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
{R : Type u_5}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(hf : QuasiMeasurePreserving f μa μb)
(c : R)
:
QuasiMeasurePreserving f (c • μa) (c • μb)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(h : QuasiMeasurePreserving f μa μb)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(h : 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 : Measure α}
{μb : Measure β}
{f : α → β}
(h : QuasiMeasurePreserving f μa μb)
{p : β → Prop}
(hg : ∀ᵐ (x : β) ∂μb, p x)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(h : QuasiMeasurePreserving f μa μb)
{g₁ g₂ : β → δ}
(hg : g₁ =ᵐ[μb] g₂)
:
@[deprecated MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp (since := "2026-08-01")]
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(h : QuasiMeasurePreserving f μa μb)
{g₁ g₂ : β → δ}
(hg : g₁ =ᵐ[μb] g₂)
:
Alias of MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp.
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
(h : 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 : Measure α}
{μb : Measure β}
{f : α → β}
{s t : Set β}
(hf : 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 : Measure α}
{μb : Measure β}
{f : α → β}
{s t : Set β}
(hf : QuasiMeasurePreserving f μa μb)
(h : s =ᵐ[μb] t)
:
theorem
MeasureTheory.NullMeasurableSet.preimage
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : Measure α}
{μb : Measure β}
{f : α → β}
{s : Set β}
(hs : NullMeasurableSet s μb)
(hf : Measure.QuasiMeasurePreserving f μa μb)
:
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.image_zpow_ae_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{e : α ≃ α}
(he : QuasiMeasurePreserving (⇑e) μ μ)
(he' : QuasiMeasurePreserving (⇑e.symm) μ μ)
(k : ℤ)
(hs : ⇑e '' s =ᵐ[μ] s)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
{f : α → α}
(hf : 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 α}
{μ : Measure α}
{s : Set α}
{f : α → α}
(hf : 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 α}
{μ : Measure α}
{s : Set α}
{f : α → α}
(h : QuasiMeasurePreserving f μ μ)
(hs : 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.pairwise_aedisjoint_of_aedisjoint_forall_ne_one
{G : Type u_5}
{α : Type u_6}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
(h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s)
(h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) => g • x) μ μ)
:
Pairwise (Function.onFun (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 α}
{μ : Measure α}
{s : Set α}
(h_ae_disjoint : ∀ (g : G), g ≠ 0 → AEDisjoint μ (g +ᵥ s) s)
(h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ)
:
Pairwise (Function.onFun (AEDisjoint μ) fun (g : G) => g +ᵥ s)
theorem
MeasureTheory.NullMeasurable.comp_quasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{ν : Measure β}
{f : α → β}
{g : β → γ}
(hg : NullMeasurable g ν)
(hf : Measure.QuasiMeasurePreserving f μ ν)
:
NullMeasurable (g ∘ f) μ
theorem
MeasureTheory.AEDisjoint.preimage
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{ν : Measure β}
{f : α → β}
{s t : Set β}
(ht : AEDisjoint ν s t)
(hf : Measure.QuasiMeasurePreserving f μ ν)
:
AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)
theorem
MeasurableEquiv.quasiMeasurePreserving_symm
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(e : α ≃ᵐ β)
: