theorem
MeasureTheory.aeMeasurable_withDensity_inv
{f : NNReal → ENNReal}
(hf : AEMeasurable f volume)
:
AEMeasurable f (volume.withDensity fun (t : NNReal) => (↑t)⁻¹)
theorem
MeasureTheory.aemeasurable_Ici_of_forall_Icc
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[LinearOrder α]
[Filter.atTop.IsCountablyGenerated]
{x : α}
{g : α → β}
(g_meas : ∀ t ≥ x, AEMeasurable g (μ.restrict (Set.Icc x t)))
:
AEMeasurable g (μ.restrict (Set.Ici x))
theorem
MeasureTheory.aemeasurable_Ici_of_forall_Icc'
{α : Type u_1}
{m0 : MeasurableSpace α}
[MeasurableSingletonClass α]
{μ : Measure α}
{β : Type u_2}
{mβ : MeasurableSpace β}
[LinearOrder α]
[Filter.atTop.IsCountablyGenerated]
{x : α}
{g : α → β}
(g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Set.Icc x t)))
:
AEMeasurable g (μ.restrict (Set.Ici x))
theorem
MeasureTheory.AEMeasurable.withDensity
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
{mβ : MeasurableSpace β}
{f : α → β}
{d : α → ENNReal}
(hf : AEMeasurable f μ)
:
AEMeasurable f (μ.withDensity d)
theorem
MeasureTheory.AEStronglyMeasurable.withDensity
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace β]
{f : α → β}
{d : α → ENNReal}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable f (μ.withDensity d)