theorem
MeasureTheory.Measure.withDensity_mono_measure
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : μ ≤ ν)
{f : α → ENNReal}
:
μ.withDensity f ≤ ν.withDensity f
theorem
MeasureTheory.Measure.rnDeriv_add_self_right
{α : Type u_1}
{mα : MeasurableSpace α}
(ν : MeasureTheory.Measure α)
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
theorem
MeasureTheory.Measure.rnDeriv_add_self_left
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
theorem
MeasureTheory.Measure.rnDeriv_eq_div
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
theorem
MeasureTheory.Measure.rnDeriv_div_rnDeriv
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{ξ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
[MeasureTheory.SigmaFinite ξ]
(hμ : μ.AbsolutelyContinuous ξ)
(hν : ν.AbsolutelyContinuous ξ)
:
theorem
MeasureTheory.Measure.rnDeriv_eq_div'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{ξ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
[MeasureTheory.SigmaFinite ξ]
(hμ : μ.AbsolutelyContinuous ξ)
(hν : ν.AbsolutelyContinuous ξ)
:
theorem
MeasureTheory.Measure.rnDeriv_eq_zero_ae_of_zero_measure
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(ν : MeasureTheory.Measure α)
{s : Set α}
(hs : MeasurableSet s)
(hμ : μ s = 0)
:
def
MeasureTheory.Measure.singularPartSet
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
Set α
Singular part set of μ with respect to ν.
Instances For
theorem
MeasureTheory.Measure.measurableSet_singularPartSet
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
:
MeasurableSet (μ.singularPartSet ν)
theorem
MeasureTheory.Measure.measure_singularPartSet
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
ν (μ.singularPartSet ν) = 0
theorem
MeasureTheory.Measure.measure_inter_compl_singularPartSet'
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{t : Set α}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.measure_inter_compl_singularPartSet
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{t : Set α}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.restrict_compl_singularPartSet_eq_withDensity
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
theorem
MeasureTheory.Measure.restrict_singularPartSet_eq_singularPart
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
μ.restrict (μ.singularPartSet ν) = μ.singularPart ν
theorem
MeasureTheory.Measure.absolutelyContinuous_restrict_compl_singularPartSet
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
(μ.restrict (μ.singularPartSet ν)ᶜ).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.rnDeriv_eq_zero_ae_of_singularPartSet
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
(ξ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
:
theorem
MeasureTheory.Measure.toReal_rnDeriv_map
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
{g : α → β}
(hg : Measurable g)
[MeasureTheory.SigmaFinite (ν.trim ⋯)]
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)]
:
(fun (a : α) => ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)).toReal) =ᵐ[ν] MeasureTheory.condexp (MeasurableSpace.comap g mβ) ν fun (a : α) => (μ.rnDeriv ν a).toReal
theorem
MeasureTheory.Measure.toReal_rnDeriv_map'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
{g : α → β}
(hg : Measurable g)
[MeasureTheory.SigmaFinite (ν.trim ⋯)]
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)]
:
(fun (a : α) => ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)).toReal) =ᵐ[ν.trim ⋯] MeasureTheory.condexp (MeasurableSpace.comap g mβ) ν fun (a : α) => (μ.rnDeriv ν a).toReal
theorem
MeasureTheory.Measure.trim_eq_map
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ mα)
:
μ.trim hm = MeasureTheory.Measure.map id μ
theorem
MeasureTheory.Measure.toReal_rnDeriv_trim_of_ac
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(hm : m ≤ mα)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.SigmaFinite ν]
[hsf : MeasureTheory.SigmaFinite (ν.trim hm)]
(hμν : μ.AbsolutelyContinuous ν)
:
(fun (x : α) => ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) =ᵐ[ν.trim hm] MeasureTheory.condexp m ν fun (x : α) => (μ.rnDeriv ν x).toReal
theorem
MeasureTheory.Measure.rnDeriv_trim_of_ac
{α : Type u_1}
{m : MeasurableSpace α}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(hm : m ≤ mα)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.SigmaFinite ν]
[MeasureTheory.SigmaFinite (ν.trim hm)]
(hμν : μ.AbsolutelyContinuous ν)
:
(μ.trim hm).rnDeriv (ν.trim hm) =ᵐ[ν.trim hm] fun (x : α) =>
ENNReal.ofReal (MeasureTheory.condexp m ν (fun (x : α) => (μ.rnDeriv ν x).toReal) x)
theorem
MeasureTheory.Measure.rnDeriv_toReal_pos
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
:
∀ᵐ (x : α) ∂μ, 0 < (μ.rnDeriv ν x).toReal
theorem
MeasureTheory.Measure.ae_rnDeriv_ne_zero_imp_of_ae_aux
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{p : α → Prop}
(h : ∀ᵐ (a : α) ∂μ, p a)
(hμν : μ.AbsolutelyContinuous ν)
:
∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a
theorem
MeasureTheory.Measure.ae_rnDeriv_ne_zero_imp_of_ae
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{p : α → Prop}
(h : ∀ᵐ (a : α) ∂μ, p a)
:
∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a
theorem
MeasureTheory.Measure.ae_eq_mul_rnDeriv_of_ae_eq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : α → MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{f : α → β → ENNReal}
{g : α → β → ENNReal}
(h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[κ a] g a)
:
theorem
MeasureTheory.Measure.ae_integrable_mul_rnDeriv_of_ae_integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : α → MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(g : α → β → ℝ)
(h : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => g a x) (κ a))
:
∀ᵐ (a : α) ∂ν, MeasureTheory.Integrable (fun (x : β) => (μ.rnDeriv ν a).toReal * g a x) (κ a)
theorem
MeasureTheory.Measure.ae_integrable_of_ae_integrable_mul_rnDeriv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{κ : α → MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
(g : α → β → ℝ)
(h : ∀ᵐ (a : α) ∂ν, MeasureTheory.Integrable (fun (x : β) => (μ.rnDeriv ν a).toReal * g a x) (κ a))
:
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (g a) (κ a)