ae_compProd_of_ae_ae — Mathlib

English

The equivalence between the a.e. property for the compProd and the pointwise a.e. property for η given κ.

Русский

Эквивалентности между свойством almost everywhere для compProd и свойством a.e. для η относительно κ.

LaTeX

$$$$ (∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc) \Leftrightarrow (∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a,b), p(b,c)). $$$$

Lean4

theorem ae_compProd_of_ae_ae {κ : Kernel α β} {η : Kernel (α × β) γ} {p : β × γ → Prop} (hp : MeasurableSet {x | p x})
    (h : ∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a, b), p (b, c)) : ∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc :=
  by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [compProd_of_not_isSFiniteKernel_left _ _ hκ]
  by_cases hη : IsSFiniteKernel η
  swap; · simp [compProd_of_not_isSFiniteKernel_right _ _ hη]
  simp_rw [ae_iff] at h ⊢
  rw [compProd_null]
  · exact h
  · exact hp.compl

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