Theorems · Theorem · geometry

EuclideanGeometry.inner_weightedVSub

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ι₁ : Type u_3} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P),
  ∑ i ∈ s₁, w₁ i = 0 →
    ∀ {ι₂ : Type u_4} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P),
      ∑ i ∈ s₂, w₂ i = 0 →
        inner ℝ ((s₁.weightedVSub p₁) w₁) ((s₂.weightedVSub p₂) w₂) =
          (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

The inner product of two vectors given with weightedVSub, in terms of the pairwise distances.

Defined in

Mathlib.Geometry.Euclidean.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor