ae_eq_zero_of_forall_setIntegral_eq_zero'

English

In the sigma-finite setting, if the integrals over all measurable sets match for f and g, then f and g are equal almost everywhere.

Русский

В сигма-финый настройке, если интегралы по всем измеримым множествам совпадают для f и g, то f и g равны почти всюду.

LaTeX

$$$$ f =_{a.e.} g $$$$

Lean4

theorem ae_eq_zero_of_forall_setIntegral_eq_zero' (hm : m ≤ m0) (f : Lp E' p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = 0)
    (hf_meas : AEStronglyMeasurable[m] f μ) : f =ᵐ[μ] 0 :=
  by
  let f_meas : lpMeas E' 𝕜 m p μ := ⟨f, hf_meas⟩
  have hf_f_meas : f =ᵐ[μ] f_meas := by simp [f_meas]
  refine hf_f_meas.trans ?_
  exact lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero hm f_meas hp_ne_zero hp_ne_top hf_int_finite hf_zero

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