ae_null_of_compProd_null — Mathlib

English

If (κ ⊗ₖ η) a s is finite, then almost surely in b under κ a, η(a,b) (Prod.mk b⁻¹' s) is finite.

Русский

Если (κ ⊗ₖ η) a s конечна, то почти наверняка по b относительно κ a выражение η(a,b)(Prod.mk b⁻¹' s) ограничено (кончно).

LaTeX

$$$$ (κ ⊗ₖ η) a s \neq ∞ \Rightarrow \text{a.e. in } b, η(a,b)(Prod.mk b^{-1}' s) < ∞. $$$$

Lean4

theorem ae_null_of_compProd_null (h : (κ ⊗ₖ η) a s = 0) : (fun b => η (a, b) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0 :=
  by
  obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
  simp_rw [compProd_null a mt] at ht
  rw [Filter.eventuallyLE_antisymm_iff]
  exact
    ⟨Filter.EventuallyLE.trans_eq (Filter.Eventually.of_forall fun x => measure_mono (Set.preimage_mono hst)) ht,
      Filter.Eventually.of_forall fun x => zero_le _⟩

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