Pullback of a measure #
In this file we define the pullback MeasureTheory.Measure.comap f μ
of a measure μ along an injective map f
such that the image of any measurable set under f is a null-measurable set.
If f does not have these properties, then we define comap f μ to be zero.
In the future, we may decide to redefine comap f μ so that it gives meaningful results, e.g.,
for covering maps like (↑) : ℝ → AddCircle (1 : ℝ).
def
MeasureTheory.Measure.comapₗ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
:
Pullback of a Measure as a linear map. If f sends each measurable set to a measurable
set, then for each measurable set s we have comapₗ f μ s = μ (f '' s).
Note that if f is not injective, this definition assigns Set.univ measure zero.
If the linearity is not needed, please use comap instead, which works for a larger class of
functions. comapₗ is an auxiliary definition and most lemmas deal with comap.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.Measure.comapₗ_apply
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
(f : α → β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s))
(μ : Measure β)
(hs : MeasurableSet s)
:
def
MeasureTheory.Measure.comap
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : Measure β)
:
Measure α
Pullback of a Measure. If f sends each measurable set to a null-measurable set,
then for each measurable set s we have comap f μ s = μ (f '' s).
Note that if f is not injective, this definition assigns Set.univ measure zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.Measure.comap_apply₀
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(μ : Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
(hs : NullMeasurableSet s (comap f μ))
:
theorem
MeasureTheory.Measure.comap_undef
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : Measure β}
(h : ¬(Function.Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ))
:
theorem
MeasureTheory.Measure.le_comap_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(μ : Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
(s : Set α)
:
theorem
MeasureTheory.Measure.comap_apply
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s))
(μ : Measure β)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.comapₗ_eq_comap
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s))
(μ : Measure β)
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(μ : Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
{s : Set α}
(hs : (comap f μ) s = 0)
:
theorem
MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(μ : Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
{s t : Set α}
(hst : s =ᶠ[ae (comap f μ)] t)
:
theorem
MeasureTheory.Measure.NullMeasurableSet.image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(μ : Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ)
(hs : NullMeasurableSet s (comap f μ))
:
NullMeasurableSet (f '' s) μ
theorem
MeasureTheory.Measure.comap_preimage
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
(μ : Measure β)
(hf : Function.Injective f)
(hf' : Measurable f)
(h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ)
{s : Set β}
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.comap_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
:
@[simp]
theorem
MeasureTheory.Measure.comap_comap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{f : α → β}
{g : β → γ}
(hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s))
(hg : Function.Injective g)
(hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s))
(μ : Measure γ)
:
theorem
MeasureTheory.Measure.comap_smul
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : Measure β}
(c : ENNReal)
:
theorem
MeasurableEmbedding.comap_add
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ ν : MeasureTheory.Measure β)
:
MeasureTheory.Measure.comap f (μ + ν) = MeasureTheory.Measure.comap f μ + MeasureTheory.Measure.comap f ν
theorem
MeasurableEquiv.comap_symm
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.map_symm
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
(e : β ≃ᵐ α)
:
theorem
MeasureTheory.Measure.comap_swap
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(μ : Measure (α × β))
: