Dot product lemmas #
A vector indexed by n can be transported along an injective map f : n → m by extending it by
zero off the range of f. Its dot product with any vector indexed by m then only sees the
coordinates in the range of f. This lets orthogonality on a subset of coordinates be read off
in the ambient coordinate space.
A nonnegative vector paired with strictly positive weights has dot product zero precisely when the vector is zero.
Main results #
Function.Injective.dotProduct_extend_zero: the dot product with a vector extended by zero along an injective map is the dot product of the pulled-back vectors.TauCeti.dotProduct_eq_zero_iff_of_pos: a nonnegative vector is zero if its pairing with strictly positive weights vanishes.
theorem
Function.Injective.dotProduct_extend_zero
{m : Type u_1}
{n : Type u_2}
{α : Type u_3}
[Fintype m]
[Fintype n]
[NonUnitalNonAssocSemiring α]
{f : n → m}
(hf : Injective f)
(x : m → α)
(y : n → α)
:
The dot product with a vector extended by zero along an injective map only sees the coordinates in the range of that map.
@[simp]
theorem
TauCeti.dotProduct_eq_zero_iff_of_pos
{ι : Type u_1}
{R : Type u_2}
[Fintype ι]
[NonUnitalNonAssocSemiring R]
[PartialOrder R]
[IsOrderedAddMonoid R]
[PosMulMono R]
[NoZeroDivisors R]
{c x : ι → R}
(hc : ∀ (i : ι), 0 < c i)
(hx : 0 ≤ x)
:
For a vector c of strictly positive weights and a nonnegative vector x, the pairing
c ⬝ᵥ x vanishes only when x does.