English
For f, under ae measurability, the ae under μ.withDensity f is equivalent to the ae under μ.restrict to {x: f(x) ≠ 0}.
Русский
Для f, при ae измеримости, ae-утверждение относительно μ.withDensity f эквивалентно ae-утверждению относительно μ.restrict на области {x: f(x) ≠ 0}.
LaTeX
$$$(\\forall^\\infty x \\partial μ.withDensity f, p x) \\iff (\\forall^\\infty x \\partial μ.restrict {x \\mid f x \\neq 0}, p x)$$$
Lean4
theorem ae_withDensity_iff_ae_restrict' {p : α → Prop} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
(∀ᵐ x ∂μ.withDensity f, p x) ↔ ∀ᵐ x ∂μ.restrict {x | f x ≠ 0}, p x :=
by
rw [ae_withDensity_iff' hf, ae_restrict_iff'₀]
· simp only [mem_setOf]
· rcases hf with ⟨g, hg, hfg⟩
have nonneg_eq_ae : {x | g x ≠ 0} =ᵐ[μ] {x | f x ≠ 0} :=
by
filter_upwards [hfg] with a ha
simp only [eq_iff_iff]
exact ⟨fun (h : g a ≠ 0) ↦ by rwa [← ha] at h, fun (h : f a ≠ 0) ↦ by rwa [ha] at h⟩
exact NullMeasurableSet.congr (MeasurableSet.nullMeasurableSet <| hg (measurableSet_singleton _)).compl nonneg_eq_ae