Pushforward of a measure #
In this file we define the pushforward MeasureTheory.Measure.map f μ
of a measure μ along an almost everywhere measurable map f.
If f is not a.e. measurable, then we define map f μ to be zero.
Main definitions #
MeasureTheory.Measure.map f μ: map of the measureμalong the mapf.
Main statements #
noncomputable def
MeasureTheory.Measure.liftLinear
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
[MeasurableSpace β]
(f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β)
(hf : ∀ (μ : MeasureTheory.Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory)
:
Lift a linear map between OuterMeasure spaces such that for each measure μ every measurable
set is caratheodory-measurable w.r.t. f μ to a linear map between Measure spaces.
Equations
- MeasureTheory.Measure.liftLinear f hf = { toFun := fun (μ : MeasureTheory.Measure α) => (f μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
MeasureTheory.Measure.liftLinear_apply₀
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
(hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
{s : Set β}
(hs : MeasureTheory.NullMeasurableSet s ((MeasureTheory.Measure.liftLinear f hf) μ))
:
((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
@[simp]
theorem
MeasureTheory.Measure.liftLinear_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
(hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
{s : Set β}
(hs : MeasurableSet s)
:
((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
theorem
MeasureTheory.Measure.le_liftLinear_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
(hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
(s : Set β)
:
(f μ.toOuterMeasure) s ≤ ((MeasureTheory.Measure.liftLinear f hf) μ) s
noncomputable def
MeasureTheory.Measure.mapₗ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
:
The pushforward of a measure as a linear map. It is defined to be 0 if f is not
a measurable function.
Equations
- MeasureTheory.Measure.mapₗ f = if hf : Measurable f then MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.map f) ⋯ else 0
Instances For
theorem
MeasureTheory.Measure.mapₗ_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
(h : f =ᵐ[μ] g)
:
(MeasureTheory.Measure.mapₗ f) μ = (MeasureTheory.Measure.mapₗ g) μ
theorem
MeasureTheory.Measure.map_def
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
@[irreducible]
noncomputable def
MeasureTheory.Measure.map
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : MeasureTheory.Measure α)
:
The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere
measurable function.
Equations
- MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
Instances For
theorem
MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
(MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ
theorem
MeasureTheory.Measure.mapₗ_apply_of_measurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(μ : MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.map_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ ν : MeasureTheory.Measure α)
{f : α → β}
(hf : Measurable f)
:
MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν
@[simp]
theorem
MeasureTheory.Measure.map_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
:
MeasureTheory.Measure.map f 0 = 0
@[simp]
theorem
MeasureTheory.Measure.map_of_not_aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : MeasureTheory.Measure α}
(hf : ¬AEMeasurable f μ)
:
MeasureTheory.Measure.map f μ = 0
theorem
AEMeasurable.of_map_ne_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.Measure.map f μ ≠ 0)
:
AEMeasurable f μ
theorem
MeasureTheory.Measure.map_congr
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f g : α → β}
(h : f =ᵐ[μ] g)
:
@[simp]
theorem
MeasureTheory.Measure.map_smul
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{R : Type u_4}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(c : R)
(μ : MeasureTheory.Measure α)
(f : α → β)
:
MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
@[deprecated MeasureTheory.Measure.map_smul (since := "2024-11-13")]
theorem
MeasureTheory.Measure.map_smul_nnreal
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(c : NNReal)
(μ : MeasureTheory.Measure α)
(f : α → β)
:
MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
theorem
MeasureTheory.Measure.map_apply₀
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.map f μ))
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
@[simp]
theorem
MeasureTheory.Measure.map_apply_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
We can evaluate the pushforward on measurable sets. For non-measurable sets, see
MeasureTheory.Measure.le_map_apply and MeasurableEquiv.map_apply.
@[simp]
theorem
MeasureTheory.Measure.map_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
theorem
MeasureTheory.Measure.map_toOuterMeasure
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
(MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim
@[simp]
theorem
MeasureTheory.Measure.map_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
MeasureTheory.Measure.map f μ = 0 ↔ μ = 0
@[simp]
theorem
MeasureTheory.Measure.mapₗ_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
:
(MeasureTheory.Measure.mapₗ f) μ = 0 ↔ μ = 0
theorem
MeasureTheory.Measure.measure_preimage_of_map_eq_self
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → α}
(hf : MeasureTheory.Measure.map f μ = μ)
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
If map f μ = μ, then the measure of the preimage of any null measurable set s
is equal to the measure of s.
Note that this lemma does not assume (a.e.) measurability of f.
theorem
MeasureTheory.Measure.map_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
MeasureTheory.Measure.map f μ ≠ 0 ↔ μ ≠ 0
theorem
MeasureTheory.Measure.mapₗ_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
:
(MeasureTheory.Measure.mapₗ f) μ ≠ 0 ↔ μ ≠ 0
@[simp]
theorem
MeasureTheory.Measure.map_id
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.map_id'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.Measure.map (fun (x : α) => x) μ = μ
theorem
MeasureTheory.Measure.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{μ : MeasureTheory.Measure α}
{g : β → γ}
{f : α → β}
(hg : Measurable g)
(hf : Measurable f)
:
MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
Mapping a measure twice is the same as mapping the measure with the composition. This version is
for measurable functions. See map_map_of_aemeasurable when they are just ae measurable.
theorem
MeasureTheory.Measure.map_mono
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : MeasureTheory.Measure α}
{f : α → β}
(h : μ ≤ ν)
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.le_map_apply
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(s : Set β)
:
μ (f ⁻¹' s) ≤ (MeasureTheory.Measure.map f μ) s
Even if s is not measurable, we can bound map f μ s from below.
See also MeasurableEquiv.map_apply.
theorem
MeasureTheory.Measure.le_map_apply_image
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(s : Set α)
:
μ s ≤ (MeasureTheory.Measure.map f μ) (f '' s)
theorem
MeasureTheory.Measure.preimage_null_of_map_null
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : (MeasureTheory.Measure.map f μ) s = 0)
:
Even if s is not measurable, map f μ s = 0 implies that μ (f ⁻¹' s) = 0.
theorem
MeasureTheory.Measure.tendsto_ae_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.mem_ae_map_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasurableSet s)
:
s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ) ↔ f ⁻¹' s ∈ MeasureTheory.ae μ
theorem
MeasureTheory.mem_ae_of_mem_ae_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ))
:
f ⁻¹' s ∈ MeasureTheory.ae μ
theorem
MeasureTheory.ae_map_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{p : β → Prop}
(hp : MeasurableSet {x : β | p x})
:
(∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
theorem
MeasureTheory.ae_of_ae_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{p : β → Prop}
(h : ∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y)
:
∀ᵐ (x : α) ∂μ, p (f x)
theorem
MeasureTheory.ae_map_mem_range
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m0 : MeasurableSpace α}
(f : α → β)
(hf : MeasurableSet (Set.range f))
(μ : MeasureTheory.Measure α)
:
∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, x ∈ Set.range f
theorem
MeasurableEmbedding.map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure α)
(s : Set β)
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
Interactions of measurable equivalences and measures
theorem
MeasurableEquiv.map_apply
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
(f : α ≃ᵐ β)
(s : Set β)
:
(MeasureTheory.Measure.map (⇑f) μ) s = μ (⇑f ⁻¹' s)
If we map a measure along a measurable equivalence, we can compute the measure on all sets (not just the measurable ones).
@[simp]
theorem
MeasurableEquiv.map_symm_map
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ
@[simp]
theorem
MeasurableEquiv.map_map_symm
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.map (⇑e.symm) ν) = ν
theorem
MeasurableEquiv.map_measurableEquiv_injective
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.map (⇑e) μ = ν ↔ MeasureTheory.Measure.map (⇑e.symm) ν = μ
theorem
MeasurableEquiv.map_ae
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(f : α ≃ᵐ β)
(μ : MeasureTheory.Measure α)
:
Filter.map (⇑f) (MeasureTheory.ae μ) = MeasureTheory.ae (MeasureTheory.Measure.map (⇑f) μ)