English
If f,g: α→ℝ≥0∞ are a.e.-equal on all finite-measure subsets and their Lp-density is finite, then f=g a.e.
Русский
Если f,g одинаковы почти повсюду на всех подмножеств помеченной меры с конечной мерой и их плотности Lp конечна, то f=g a.e.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$
Lean4
theorem lintegral_eq_lintegral_of_isPiSystem (h_eq : m0 = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s)
(basic : ∀ t ∈ s, ∫⁻ x in t, f x ∂μ = ∫⁻ x in t, g x ∂μ) (h_univ : ∫⁻ x, f x ∂μ = ∫⁻ x, g x ∂μ)
(hf_int : ∫⁻ x, f x ∂μ ≠ ∞) : ∀ t (_ : MeasurableSet t), ∫⁻ x in t, f x ∂μ = ∫⁻ x in t, g x ∂μ :=
by
refine MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_
· simp
· intro t ht h_eq
rw [setLIntegral_compl ht, setLIntegral_compl ht, h_eq, h_univ]
· refine ne_of_lt ?_
calc
∫⁻ x in t, g x ∂μ
_ ≤ ∫⁻ x, g x ∂μ := (setLIntegral_le_lintegral t _)
_ < ∞ := by rw [← h_univ]; exact hf_int.lt_top
· refine ne_of_lt ?_
calc
∫⁻ x in t, f x ∂μ
_ ≤ ∫⁻ x, f x ∂μ := (setLIntegral_le_lintegral t _)
_ < ∞ := hf_int.lt_top
· intro t htd htm h
simp_rw [lintegral_iUnion htm htd, h]
