compProd_left — Mathlib

English

A simplified form of associativity: (μ ⊗ₘ κ) ⊗ₘ η equals μ ⊗ₘ (κ ⊗ₖ η) after applying prodAssoc.

Русский

Упрощённая форма ассоциативности: (μ ⊗ₘ κ) ⊗ₘ η равна μ ⊗ₘ (κ ⊗ₖ η) после применения prodAssoc.

LaTeX

$$$(\\mu \\otimes_m \\kappa) \\otimes_m \\eta = \\text{map}(\\mathrm{prodAssoc})(\\mu \\otimes_m (\\kappa \\otimes_k \\eta))$$$

Lean4

theorem compProd_left [SFinite ν] (hμν : μ ≪ ν) (κ : Kernel α β) : μ ⊗ₘ κ ≪ ν ⊗ₘ κ :=
  by
  by_cases hκ : IsSFiniteKernel κ
  · have : SFinite μ := sFinite_of_absolutelyContinuous hμν
    refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
    rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)] at hs_zero ⊢
    exact hμν.ae_eq hs_zero
  · simp [compProd_of_not_isSFiniteKernel _ _ hκ]

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