Theorems · Theorem · functional analysis

inner_sum_smul_sum_smul_of_sum_eq_zero

∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {ι₁ : Type u_4} {s₁ : Finset ι₁}
  {w₁ : ι₁ → ℝ} (v₁ : ι₁ → F),
  ∑ i ∈ s₁, w₁ i = 0 →
    ∀ {ι₂ : Type u_5} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (v₂ : ι₂ → F),
      ∑ i ∈ s₂, w₂ i = 0 →
        inner ℝ (∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁) (∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂) =
          (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

The inner product of two weighted sums, where the weights in each sum add to 0, in terms of the norms of pairwise differences.

Defined in

Mathlib.Analysis.InnerProductSpace.Basic

Cited by

1 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupInnerProductSpace