ae_withDensity_iff_ae_restrict' — Mathlib

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

Похожие утверждения