Absolute Continuity of Measures #
We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν,
if ν(A) = 0 implies that μ(A) = 0. We denote that by μ ≪ ν.
It is equivalent to an inequality of the almost everywhere filters of the measures:
μ ≪ ν ↔ ae μ ≤ ae ν.
Main definitions #
MeasureTheory.Measure.AbsolutelyContinuous μ ν:μis absolutely continuous with respect toν
Main statements #
ae_le_iff_absolutelyContinuous:ae μ ≤ ae ν ↔ μ ≪ ν
Notation #
μ ≪ ν:MeasureTheory.Measure.AbsolutelyContinuous μ ν. That is:μis absolutely continuous with respect toν
def
MeasureTheory.Measure.AbsolutelyContinuous
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ ν : Measure α)
:
We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν,
if ν(A) = 0 implies that μ(A) = 0.
Equations
- μ.AbsolutelyContinuous ν = ∀ ⦃s : Set α⦄, ν s = 0 → μ s = 0
Instances For
We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν,
if ν(A) = 0 implies that μ(A) = 0.
Equations
- MeasureTheory.«term_≪_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_≪_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪ ") (Lean.ParserDescr.cat `term 51))
Instances For
theorem
MeasureTheory.Measure.absolutelyContinuous_of_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
(h : μ ≤ ν)
:
theorem
LE.le.absolutelyContinuous
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ ≤ ν)
:
theorem
MeasureTheory.Measure.absolutelyContinuous_of_eq
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
(h : μ = ν)
:
theorem
Eq.absolutelyContinuous
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ = ν)
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.mk
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
(h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0)
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.refl
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : Measure α)
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.rfl
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
:
instance
MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl
{α : Type u_1}
{x✝ : MeasurableSpace α}
:
IsRefl (Measure α) fun (x1 x2 : Measure α) => x1.AbsolutelyContinuous x2
@[simp]
theorem
MeasureTheory.Measure.AbsolutelyContinuous.zero
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : Measure α)
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.trans
{α : Type u_1}
{mα : MeasurableSpace α}
{μ₁ μ₂ μ₃ : Measure α}
(h1 : μ₁.AbsolutelyContinuous μ₂)
(h2 : μ₂.AbsolutelyContinuous μ₃)
:
μ₁.AbsolutelyContinuous μ₃
theorem
MeasureTheory.Measure.AbsolutelyContinuous.map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : Measure α}
(h : μ.AbsolutelyContinuous ν)
{f : α → β}
(hf : Measurable f)
:
(map f μ).AbsolutelyContinuous (map f ν)
theorem
MeasureTheory.Measure.AbsolutelyContinuous.smul_left
{α : Type u_1}
{R : Type u_5}
{mα : MeasurableSpace α}
{μ ν : Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : μ.AbsolutelyContinuous ν)
(c : R)
:
(c • μ).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.smul
{α : Type u_1}
{R : Type u_5}
{mα : MeasurableSpace α}
{μ ν : Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : μ.AbsolutelyContinuous ν)
(c : R)
:
(c • μ).AbsolutelyContinuous (c • ν)
If μ ≪ ν, then c • μ ≪ c • ν.
Earlier, this name was used for what's now called AbsolutelyContinuous.smul_left.
@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.smul (since := "2024-11-14")]
theorem
MeasureTheory.Measure.AbsolutelyContinuous.smul_both
{α : Type u_1}
{R : Type u_5}
{mα : MeasurableSpace α}
{μ ν : Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : μ.AbsolutelyContinuous ν)
(c : R)
:
(c • μ).AbsolutelyContinuous (c • ν)
Alias of MeasureTheory.Measure.AbsolutelyContinuous.smul.
If μ ≪ ν, then c • μ ≪ c • ν.
Earlier, this name was used for what's now called AbsolutelyContinuous.smul_left.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add
{α : Type u_1}
{mα : MeasurableSpace α}
{μ₁ μ₂ ν ν' : Measure α}
(h1 : μ₁.AbsolutelyContinuous ν)
(h2 : μ₂.AbsolutelyContinuous ν')
:
(μ₁ + μ₂).AbsolutelyContinuous (ν + ν')
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ₁ μ₂ ν : Measure α}
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add_left
{α : Type u_1}
{mα : MeasurableSpace α}
{μ₁ μ₂ ν : Measure α}
(h₁ : μ₁.AbsolutelyContinuous ν)
(h₂ : μ₂.AbsolutelyContinuous ν)
:
(μ₁ + μ₂).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add_right
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
(h1 : μ.AbsolutelyContinuous ν)
(ν' : Measure α)
:
μ.AbsolutelyContinuous (ν + ν')
@[simp]
theorem
MeasureTheory.Measure.absolutelyContinuous_zero_iff
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
:
theorem
MeasureTheory.Measure.absolutelyContinuous_refl
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : Measure α)
:
theorem
MeasureTheory.Measure.absolutelyContinuous_rfl
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
:
theorem
MeasureTheory.Measure.absolutelyContinuous_sum_left
{α : Type u_1}
{ι : Type u_4}
{mα : MeasurableSpace α}
{ν : Measure α}
{μs : ι → Measure α}
(hμs : ∀ (i : ι), (μs i).AbsolutelyContinuous ν)
:
(sum μs).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.absolutelyContinuous_sum_right
{α : Type u_1}
{ι : Type u_4}
{mα : MeasurableSpace α}
{ν : Measure α}
{μs : ι → Measure α}
(i : ι)
(hνμ : ν.AbsolutelyContinuous (μs i))
:
ν.AbsolutelyContinuous (sum μs)
theorem
MeasureTheory.Measure.smul_absolutelyContinuous
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{c : ENNReal}
:
(c • μ).AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.absolutelyContinuous_of_le_smul
{α : Type u_1}
{mα : MeasurableSpace α}
{μ μ' : Measure α}
{c : ENNReal}
(hμ'_le : μ' ≤ c • μ)
:
μ'.AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.absolutelyContinuous_smul
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{c : ENNReal}
(hc : c ≠ 0)
:
μ.AbsolutelyContinuous (c • μ)
theorem
MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
:
theorem
LE.le.absolutelyContinuous_of_ae
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
Alias of the forward direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.ae_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
:
μ.AbsolutelyContinuous ν → ae μ ≤ ae ν
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
theorem
MeasureTheory.Measure.ae_mono'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
:
μ.AbsolutelyContinuous ν → ae μ ≤ ae ν
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
{α : Type u_1}
{δ : Type u_3}
{mα : MeasurableSpace α}
{μ ν : Measure α}
(h : μ.AbsolutelyContinuous ν)
{f g : α → δ}
(h' : f =ᶠ[ae ν] g)
:
theorem
MeasureTheory.AEDisjoint.of_absolutelyContinuous
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
{ν : Measure α}
(h' : ν.AbsolutelyContinuous μ)
:
AEDisjoint ν s t
theorem
MeasureTheory.AEDisjoint.of_le
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
{s t : Set α}
(h : AEDisjoint μ s t)
{ν : Measure α}
(h' : ν ≤ μ)
:
AEDisjoint ν s t
theorem
MeasureTheory.ae_mono
{α : Type u_1}
{mα : MeasurableSpace α}
{μ ν : Measure α}
(h : μ ≤ ν)
:
theorem
MeasurableEmbedding.absolutelyContinuous_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
{μ ν : MeasureTheory.Measure α}
(hf : MeasurableEmbedding f)
(hμν : μ.AbsolutelyContinuous ν)
: