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))
(μ : MeasureTheory.Measure β)
(hs : MeasurableSet s)
:
((MeasureTheory.Measure.comapₗ f) μ) s = μ (f '' s)
def
MeasureTheory.Measure.comap
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : MeasureTheory.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 α}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(μ : MeasureTheory.Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ)
(hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ))
:
(MeasureTheory.Measure.comap f μ) s = μ (f '' s)
theorem
MeasureTheory.Measure.le_comap_apply
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(μ : MeasureTheory.Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ)
(s : Set α)
:
μ (f '' s) ≤ (MeasureTheory.Measure.comap f μ) s
theorem
MeasureTheory.Measure.comap_apply
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s))
(μ : MeasureTheory.Measure β)
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.comap f μ) s = μ (f '' s)
theorem
MeasureTheory.Measure.comapₗ_eq_comap
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s))
(μ : MeasureTheory.Measure β)
(hs : MeasurableSet s)
:
((MeasureTheory.Measure.comapₗ f) μ) s = (MeasureTheory.Measure.comap f μ) s
theorem
MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(μ : MeasureTheory.Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ)
{s : Set α}
(hs : (MeasureTheory.Measure.comap f μ) s = 0)
:
theorem
MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(μ : MeasureTheory.Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ)
{s t : Set α}
(hst : s =ᵐ[MeasureTheory.Measure.comap f μ] t)
:
theorem
MeasureTheory.Measure.NullMeasurableSet.image
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(μ : MeasureTheory.Measure β)
(hfi : Function.Injective f)
(hf : ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ)
(hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ))
:
MeasureTheory.NullMeasurableSet (f '' s) μ
theorem
MeasureTheory.Measure.comap_preimage
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
(μ : MeasureTheory.Measure β)
(hf : Function.Injective f)
(hf' : Measurable f)
(h : ∀ (t : Set α), MeasurableSet t → MeasureTheory.NullMeasurableSet (f '' t) μ)
{s : Set β}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ Set.range f)
@[simp]
theorem
MeasureTheory.Measure.comap_zero
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(f : α → β)
:
MeasureTheory.Measure.comap f 0 = 0
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 : α ≃ᵐ β)
:
MeasureTheory.Measure.comap (⇑e.symm) μ = MeasureTheory.Measure.map (⇑e) μ
theorem
MeasurableEquiv.map_symm
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
(e : β ≃ᵐ α)
:
MeasureTheory.Measure.map (⇑e.symm) μ = MeasureTheory.Measure.comap (⇑e) μ
theorem
comap_swap
{α : Type u_1}
{β : Type u_2}
{ma : MeasurableSpace α}
{mb : MeasurableSpace β}
(μ : MeasureTheory.Measure (α × β))
:
MeasureTheory.Measure.comap Prod.swap μ = MeasureTheory.Measure.map Prod.swap μ