ae_eq_zero_of_forall_setIntegral_eq_zero

English

If f is integrable and its integral over every finite-measure measurable set is zero, then f equals zero almost everywhere.

Русский

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

LaTeX

$$$$ f =^{\mathrm{ae}}_{\mu} 0 $$$$

Lean4

theorem ae_eq_zero_of_forall_setIntegral_eq_zero {f : α → E} (hf : Integrable f μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0 :=
  by
  have hf_Lp : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
  let f_Lp := hf_Lp.toLp f
  have hf_f_Lp : f =ᵐ[μ] f_Lp := (MemLp.coeFn_toLp hf_Lp).symm
  refine hf_f_Lp.trans ?_
  refine Lp.ae_eq_zero_of_forall_setIntegral_eq_zero f_Lp one_ne_zero ENNReal.coe_ne_top ?_ ?_
  · exact fun s _ _ => Integrable.integrableOn (L1.integrable_coeFn _)
  · intro s hs hμs
    rw [integral_congr_ae (ae_restrict_of_ae hf_f_Lp.symm)]
    exact hf_zero s hs hμs

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