English
For countable δ, a function g: α → Π a, X a is AEMeasurable with respect to μ iff for all a, the coordinate function x ↦ g(x)(a) is AEMeasurable with respect to μ.
Русский
Для счетного множества δ функция g: α → Π a, X a является AEMeasurable относительно μ тогда и только тогда, когда для каждого a координатная функция x ↦ g(x)(a) является AEMеасимируемой относительно μ.
LaTeX
$$$AEMeasurable\ g\ \mu \iff \forall a, AEMeasurable(\lambda x. g x a)\ \mu$$$
Lean4
theorem aemeasurable_pi_iff {g : α → Π a, X a} : AEMeasurable g μ ↔ ∀ a, AEMeasurable (fun x ↦ g x a) μ :=
by
constructor
· exact AEMeasurable.eval
· intro h
use fun x a ↦ (h a).mk _ x, measurable_pi_lambda _ fun a ↦ (h a).measurable_mk
exact (eventually_countable_forall.mpr fun a ↦ (h a).ae_eq_mk).mono fun _ h ↦ funext h
