compProd_of_left — Mathlib

English

If μ ⟂ ν, then μ ⊗ κ ⟂ ν ⊗ η for any kernels κ, η.

Русский

Если μ ⟂ ν, тогда μ ⊗ κ ⟂ ν ⊗ η для любых ядер κ, η.

LaTeX

$$$(μ ⊗ₘ κ) ⟂ₘ (ν ⊗ₘ η)$$$

Lean4

theorem compProd_of_left (hμν : μ ⟂ₘ ν) (κ η : Kernel α β) : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η :=
  by
  by_cases hμ : SFinite μ
  swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
  by_cases hν : SFinite ν
  swap; · rw [compProd_of_not_sfinite _ _ hν]; simp
  by_cases hκ : IsSFiniteKernel κ
  swap; · rw [compProd_of_not_isSFiniteKernel _ _ hκ]; simp
  by_cases hη : IsSFiniteKernel η
  swap; · rw [compProd_of_not_isSFiniteKernel _ _ hη]; simp
  refine ⟨hμν.nullSet ×ˢ univ, hμν.measurableSet_nullSet.prod .univ, ?_⟩
  rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union]
  simp only [MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ, prod_empty, union_empty, true_and]
  rw [compProd_apply_prod hμν.measurableSet_nullSet.compl .univ]
  simp

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