wInner_cWeight_eq_smul_wInner_one

English

With uniform weight cWeight, the weighted inner product equals (card ι)^{-1} times the unweighted inner product.

Русский

При равномерных весах cWeight скалярное произведение равно (карта ι)^{-1} умноженному на незатяженное произведение.

LaTeX

$$$ \\langle f, g \\rangle_{𝕜,[w]} = (|ι|)^{-1} \\langle f, g \\rangle_{𝕜,[1]} $$$

Lean4

theorem wInner_cWeight_eq_smul_wInner_one (f g : ∀ i, E i) : ⟪f, g⟫ₙ_[𝕜] = (Fintype.card ι : ℚ≥0)⁻¹ • ⟪f, g⟫_[𝕜] := by
  simp [wInner, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]

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