ae_nonneg_restrict_of_forall_setIntegral_nonneg

English

If two functions f and g have equal integrals over every measurable set, then they are equal almost everywhere.

Русский

Если интегралы функций f и g по каждому измеримому множеству равны, то f = g a.e.

LaTeX

$$$\forall s, \ MeasurableSet(s) \Rightarrow ∫_s f = ∫_s g \Rightarrow f = g \ a.e.$$$

Lean4

theorem ae_nonneg_restrict_of_forall_setIntegral_nonneg {f : α → ℝ}
    (hf_int_finite : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn f s μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) {t : Set α} (ht : MeasurableSet t)
    (hμt : μ t ≠ ∞) : 0 ≤ᵐ[μ.restrict t] f :=
  by
  refine
    ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) fun s hs _ =>
      ?_
  refine hf_zero (s ∩ t) (hs.inter ht) ?_
  exact (measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμt)

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