English
If two a.e.-measurable functions on a product space have finite integrals and agree on all rectangle sets, then they are a.e. equal.
Русский
Если две a.e.-измеримые функции на произведении пространств имеют конечные интегралы и согласованы по всем прямоугольникам, тогда они равны почти повсюду.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$
Lean4
/-- If two a.e.-measurable functions `α × β → ℝ≥0∞` with finite integrals have the same integral
on every rectangle, then they are almost everywhere equal. -/
theorem ae_eq_of_setLIntegral_prod_eq {β : Type*} {mβ : MeasurableSpace β} {μ : Measure (α × β)} {f g : α × β → ℝ≥0∞}
(hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hf_int : ∫⁻ x, f x ∂μ ≠ ∞)
(h :
∀ ⦃s : Set α⦄ (_ : MeasurableSet s) ⦃t : Set β⦄ (_ : MeasurableSet t),
∫⁻ x in s ×ˢ t, f x ∂μ = ∫⁻ x in s ×ˢ t, g x ∂μ) :
f =ᵐ[μ] g :=
by
have hg_int : ∫⁻ x, g x ∂μ ≠ ∞ := by
rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ, setLIntegral_univ]
refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hf_int hg_int fun s hs _ ↦ ?_
refine lintegral_eq_lintegral_of_isPiSystem_of_univ_mem generateFrom_prod.symm isPiSystem_prod ?_ ?_ hf_int hs
· exact ⟨Set.univ, .univ, Set.univ, .univ, Set.univ_prod_univ⟩
· rintro _ ⟨s, hs, t, ht, rfl⟩
exact h hs ht
