English
If two functions on a product space have equal set-L-integrals on all rectangles from a Pi-system that generates the product σ-algebra, then they are equal a.e.
Русский
Если две функции на произведении пространств имеют равные интегралы по всем прямоугольникам из Π-системы, порождающей произведение σ-алгебру, то они равны почти повсюду.
LaTeX
$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$
Lean4
/-- If we have the additional hypothesis `∀ᵐ x ∂μ, p x (fun n ↦ f n x)`, this is a measurable set
whose complement has measure 0 such that for all `x ∈ aeSeqSet`, `f i x` is equal to
`(hf i).mk (f i) x` for all `i` and we have the pointwise property `p x (fun n ↦ f n x)`. -/
def aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) (p : α → (ι → β) → Prop) : Set α :=
(toMeasurable μ {x | (∀ i, f i x = (hf i).mk (f i) x) ∧ p x fun n => f n x}ᶜ)ᶜ
