wInner_one_const_left — Mathlib

English

For weight w ≡ 1, the weighted inner product equals the standard inner product on the direct sum, i.e., ⟪f, g⟫_{𝕜,1} = ⟪WithLp.toLp 2 f, WithLp.toLp 2 g⟫.

Русский

При весе w ≡ 1 взвешенное скалярное произведение совпадает с обычным скалярным на сумме, т. е. ⟪f,g⟫_{𝕜,1} = ⟪WithLp.toLp 2 f, WithLp.toLp 2 g⟫.

LaTeX

$$$⟪f, g⟫_{𝕜, 1} = ⟪WithLp.toLp 2 f, WithLp.toLp 2 g⟫_{𝕜}$$$

Lean4

@[simp]
theorem wInner_one_const_left (a : 𝕜) (f : ι → 𝕜) : ⟪const _ a, f⟫_[𝕜] = (∑ i, f i) * conj a := by
  simp [wInner_one_eq_sum, sum_mul]

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