wInner_cWeight_eq_expect — Mathlib

English

The weighted inner product equals the expectation of the coordinate-wise inner products, i.e., ⟪f, g⟫_{𝕜} = 𝔼 i ⟪f_i, g_i⟫_{𝕜}.

Русский

Взвешенное скалярное произведение равно математическому ожиданию скалярных произведений по координатам: ⟪f, g⟫ = 𝔼_i ⟪f_i, g_i⟫.

LaTeX

$$$⟪f, g⟫_{𝕜} = \mathbb{E}_i \;⟪f_i, g_i\⟫_{𝕜}$$$

Lean4

theorem wInner_cWeight_eq_expect (f g : ∀ i, E i) : ⟪f, g⟫ₙ_[𝕜] = 𝔼 i, ⟪f i, g i⟫_𝕜 := by
  simp [wInner, expect, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]

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