lintegral_eq_lintegral_of_isPiSystem_of_univ_mem

English

If f,g: α→ℝ≥0∞ are AEMeasurable and ∀ s finite, ∫_s f = ∫_s g, then f=g a.e.

Русский

Если f,g – AEMеасeable и для всех конечных s имеем ∫_s f = ∫_s g, то f=g a.e.

LaTeX

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

Lean4

theorem lintegral_eq_lintegral_of_isPiSystem_of_univ_mem (h_eq : m0 = MeasurableSpace.generateFrom s)
    (h_inter : IsPiSystem s) (h_univ : Set.univ ∈ s) (basic : ∀ t ∈ s, ∫⁻ x in t, f x ∂μ = ∫⁻ x in t, g x ∂μ)
    (hf_int : ∫⁻ x, f x ∂μ ≠ ∞) {t : Set α} (ht : MeasurableSet t) : ∫⁻ x in t, f x ∂μ = ∫⁻ x in t, g x ∂μ :=
  by
  refine lintegral_eq_lintegral_of_isPiSystem h_eq h_inter basic ?_ hf_int t ht
  rw [← setLIntegral_univ, ← setLIntegral_univ g]
  exact basic _ h_univ

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