English
If densities d are ae-positive, then equality of functions f and g with respect to μ.withDensity d is equivalent to equality with respect to μ.
Русский
Если плотности d a.e. положительны, то равенство f и g относительно μ.withDensity d эквивалентно равенству относительно μ.
LaTeX
$$$f =ᵐ[μ.withDensity d] g \iff f =ᵐ[μ] g$ under nonzero a.e. conditions.$$
Lean4
/-- If `μ` is an `s`-finite measure, then so is `μ.withDensity f`. -/
instance instSFinite [SFinite μ] {f : α → ℝ≥0∞} : SFinite (μ.withDensity f) :=
by
wlog hfm : Measurable f generalizing f
· rcases exists_measurable_le_withDensity_eq μ f with ⟨g, hgm, -, h⟩
exact h ▸ this hgm
wlog hμ : IsFiniteMeasure μ generalizing μ
· rw [← sum_sfiniteSeq μ, withDensity_sum]
have (n : ℕ) : SFinite ((sfiniteSeq μ n).withDensity f) := this inferInstance
infer_instance
set s := {x | f x = ∞}
have hs : MeasurableSet s := hfm (measurableSet_singleton _)
have key :=
calc
μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) := by
simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]
_ = μ.withDensity (sᶜ.indicator f) + .sum fun _ : ℕ ↦ μ.withDensity (s.indicator 1) :=
by
rw [← withDensity_tsum (by measurability)]
congr 2 with x
rw [ENNReal.tsum_apply]
if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero] else simp [hx]
have : SigmaFinite (μ.withDensity (sᶜ.indicator f)) :=
by
refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_
simp [indicator_apply, ite_eq_iff, s] at hx
have : SigmaFinite (μ.withDensity (s.indicator 1)) :=
by
rw [withDensity_indicator hs]
exact SigmaFinite.withDensity 1
rw [key]
infer_instance
