mutuallySingular_compProd_right_iff

English

For finite κ, η kernels, μ finite (SFinite), we have (μ ⊗ κ) ⟂ (μ ⊗ η) if and only if κ a ⟂ η a for μ-almost every a.

Русский

Для конечных ядер κ, η и μ (SFinite) имеем: μ ⊗ κ взаимно-селективно пер μ ⊗ η тогда и только тогда, когда κ(a) ⟂ η(a) для μ-почти всех a.

LaTeX

$$$(μ \\otimes κ) \\perp (μ \\otimes η) \\quad\\iff\\quad \\forall^{\\text{ae}} a\\partial μ,\\ κ(a) \\perp_m η(a).$$$

Lean4

theorem mutuallySingular_compProd_right_iff [SFinite μ] : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ⟂ₘ η a :=
  ⟨fun h ↦ mutuallySingular_of_mutuallySingular_compProd h AbsolutelyContinuous.rfl AbsolutelyContinuous.rfl,
    MutuallySingular.compProd_of_right _ _⟩

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