variance_dual_prod' — Mathlib

English

Let L be a dual, μ and ν probability measures. Then Var[L; μ×ν] equals Var[component; μ] + Var[component; ν].

Русский

Пусть L — двойственный функционал, μ и ν — вероятностные меры. Тогда Var[L; μ×ν] равна сумме дисперсий по компонентам.

LaTeX

$$$\operatorname{Var}[L;\, \mu\times\nu] = \operatorname{Var}[L;\text{inl};\mu] + \operatorname{Var}[L;\text{inr};\nu]$$$

Lean4

theorem variance_dual_prod' {L : StrongDual ℝ (E × F)} (hLμ : MemLp (L.comp (.inl ℝ E F)) 2 μ)
    (hLν : MemLp (L.comp (.inr ℝ E F)) 2 ν) :
    Var[L; μ.prod ν] = Var[L.comp (.inl ℝ E F); μ] + Var[L.comp (.inr ℝ E F); ν] :=
  by
  have : L = fun x : E × F ↦ L.comp (.inl ℝ E F) x.1 + L.comp (.inr ℝ E F) x.2 := by ext; rw [L.comp_inl_add_comp_inr]
  rw [this, variance_add_prod hLμ hLν]

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