Documentation

TestingLowerBounds.ForMathlib.RnDeriv

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

Singular part set of μ with respect to ν.

Equations
  • μ.singularPartSet ν = {x : α | ν.rnDeriv (μ + ν) x = 0}
Instances For
    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 ) ν 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 ) ν fun (a : α) => (μ.rnDeriv ν a).toReal
    theorem MeasureTheory.Measure.trim_eq_map {α : Type u_1} {m : MeasurableSpace α} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : 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 ) [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 ) [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 0p 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 0p 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)