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 ν] : ν.rnDeriv (μ + ν) =ᵐ[ν] fun (x : α) => (μ.rnDeriv ν x + 1)⁻¹

theorem MeasureTheory.Measure.rnDeriv_add_self_left {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : μ.rnDeriv (μ + ν) =ᵐ[ν] fun (x : α) => μ.rnDeriv ν x / (μ.rnDeriv ν x + 1)

theorem MeasureTheory.Measure.rnDeriv_eq_div {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : μ.rnDeriv ν =ᵐ[ν] fun (x : α) => μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

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 ξ) : (fun (x : α) => μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun (x : α) => μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

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 ξ) : μ.rnDeriv ν =ᵐ[ν] fun (x : α) => μ.rnDeriv ξ x / ν.rnDeriv ξ x

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) : ∀ᵐ (x : α) ∂ν, x ∈ s → μ.rnDeriv ν x = 0

def MeasureTheory.Measure.singularPartSet {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : Set α

Singular part set of μ with respect to ν.

Equations

• μ.singularPartSet ν = {x : α | ν.rnDeriv (μ + ν) x = 0}

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) : μ (t ∩ (μ.singularPartSet ν)ᶜ) = ∫⁻ (x : α) in t ∩ (μ.singularPartSet ν)ᶜ, μ.rnDeriv ν x ∂ν

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) : μ (t ∩ (μ.singularPartSet ν)ᶜ) = ∫⁻ (x : α) in t, μ.rnDeriv ν x ∂ν

theorem MeasureTheory.Measure.restrict_compl_singularPartSet_eq_withDensity {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : μ.restrict (μ.singularPartSet ν)ᶜ = ν.withDensity (μ.rnDeriv ν)

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 ν] : ∀ᵐ (x : α) ∂ξ, x ∈ μ.singularPartSet ν → ν.rnDeriv ξ x = 0

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) : ∀ᵐ (a : α) ∂ν, (fun (b : β) => μ.rnDeriv ν a * f a b) =ᵐ[κ a] fun (b : β) => μ.rnDeriv ν a * g a b

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)