Definitions and lemmas for Vector

accumulateProducts separates product accumulation from reduction. Its reduction theorem recovers dotProduct whenever reduction preserves zero, addition, and the chosen products.

def Vector.induction₂_temp {α : Type u_2} {β : Type u_3} {motive : {n : ℕ} → Vector α n → Vector β n → Sort u_1} (v_empty : motive #v[] #v[]) (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → (hd' : β) → (tl' : Vector β n) → motive tl tl' → motive (tl.insertIdx 0 hd ⋯) (tl'.insertIdx 0 hd' ⋯)) {m : ℕ} (v : Vector α m) (v' : Vector β m) : motive v v'

def Vector.nil {α : Type u_1} : Vector α 0

The empty vector.

def Vector.cons {α : Type u_1} {n : ℕ} (hd : α) (tl : Vector α n) : Vector α (n + 1)

Construct a vector by prepending an element to the front of a vector, using insertIdx at 0.

@[simp]

theorem Vector.head_cons {α : Type u_1} {n : ℕ} (hd : α) (tl : Vector α n) : (cons hd tl).head = hd

theorem Vector.cons_get_eq {α : Type u_1} {n : ℕ} (hd : α) (tl : Vector α n) (i : Fin (n + 1)) : (cons hd tl).get i = if hi : (↑i == 0) = true then hd else tl.get ⟨↑i - 1, ⋯⟩

@[simp]

theorem Vector.cons_empty_tail_eq_nil {α : Type u_1} (hd : α) (tl : Vector α 0) : cons hd tl = #v[hd]

@[simp]

theorem Vector.tail_cons {α : Type u_1} {n : ℕ} (hd : α) (tl : Vector α n) : (cons hd tl).tail = tl

@[simp]

theorem Vector.cons_toList_eq_List_cons {α : Type u_1} {n : ℕ} (hd : α) (tl : Vector α n) : (cons hd tl).toList = hd :: tl.toList

theorem Vector.foldl_eq_toList_foldl {α : Type u_1} {β : Type u_2} {n : ℕ} (f : β → α → β) (init : β) (v : Vector α n) : foldl f init v = List.foldl f init v.toList

theorem Vector.foldl_succ {α : Type u_1} {β : Type u_2} {n : ℕ} [NeZero n] (f : β → α → β) (init : β) (v : Vector α n) : foldl f init v = foldl f (f init v.head) v.tail

theorem Vector.zipWith_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (a : α) (b : Vector α n) (c : β) (d : Vector β n) : zipWith f (cons a b) (cons c d) = cons (f a c) (zipWith f b d)

def Vector.dotProduct {R : Type u_1} {n : ℕ} [Zero R] [Add R] [Mul R] (a b : Vector R n) : R

Inner product between two vectors of the same size. Should be faster than _root_.dotProduct due to efficient operations on Vectors.

def Vector.«term_*ᵥ_» : Lean.TrailingParserDescr

Inner product between two vectors of the same size. Should be faster than _root_.dotProduct due to efficient operations on Vectors.

def Vector.accumulateProducts {R : Type u_1} {n : ℕ} {W : Type u_2} [Add W] (product : R → R → W) (init : W) (a b : Vector R n) : W

Accumulate paired products from equal-length vectors, from left to right, starting at init. The products and accumulator lie in W; no reduction is performed.

theorem Vector.reduce_accumulateProducts {R : Type u_1} {n : ℕ} {W : Type u_2} [AddZero W] [AddMonoid R] [Mul R] (reduce : W →+ R) (product : R → R → W) (hproduct : ∀ (x y : R), reduce (product x y) = x * y) (init : W) (a b : Vector R n) : reduce (accumulateProducts product init a b) = reduce init + a.dotProduct b

If reduction preserves addition and each paired product, reducing the accumulator gives the reduced initial value plus the dot product of the input vectors.

theorem Vector.reduce_accumulateProducts_zero {R : Type u_1} {n : ℕ} {W : Type u_2} [AddZero W] [AddMonoid R] [Mul R] (reduce : W →+ R) (product : R → R → W) (hproduct : ∀ (x y : R), reduce (product x y) = x * y) (a b : Vector R n) : reduce (accumulateProducts product 0 a b) = a.dotProduct b

Reducing a product accumulator initialized at zero recovers the dot product.

theorem Vector.accumulateProducts_mul {R : Type u_1} {n : ℕ} [AddMonoid R] [Mul R] (init : R) (a b : Vector R n) : accumulateProducts (fun (x1 x2 : R) => x1 * x2) init a b = init + a.dotProduct b

Ordinary multiplication is an eager product accumulator, with identity reduction.

@[simp]

theorem Vector.dotProduct_cons {R : Type u_1} {n : ℕ} [AddCommMonoid R] [Mul R] (a : R) (b : Vector R n) (c : R) (d : Vector R n) : (cons a b).dotProduct (cons c d) = a * c + b.dotProduct d

def Vector.Matrix (α : Type u_2) (m n : ℕ) : Type u_2

A matrix represented as iterated vectors in row-major order. m is the number of rows, and n is the number of columns

def Vector.Matrix.mulVec {α : Type u_2} [Zero α] [Add α] [Mul α] {numRows numCols : ℕ} (M : Vector (Vector α numCols) numRows) (x : Vector α numCols) : Vector α numRows

Matrix-vector multiplication over α. M is given as a vector of row-vectors.

def Vector.Matrix.ofFlatten {α : Type u_2} {m n : ℕ} (v : Vector α (m * n)) : Matrix α m n

Convert a flat row-major vector of length m*n into an m × n row-major matrix represented as Vector (Vector α n) m.

def Vector.Matrix.toFinMatrix {α : Type u_2} {m n : ℕ} (matrix : Matrix α m n) : _root_.Matrix (Fin m) (Fin n) α

Convert to a Fin-indexed matrix (the definition in Mathlib): Fin m → Fin n → α

def Vector.Matrix.ofFinMatrix {α : Type u_2} {m n : ℕ} (matrix : _root_.Matrix (Fin m) (Fin n) α) : Matrix α m n

Convert from a Fin-indexed matrix (the definition in Mathlib): Fin m → Fin n → α

def Vector.Matrix.transpose {α : Type u_2} {m n : ℕ} (matrix : Matrix α m n) : Matrix α n m

Transpose a matrix by swapping rows and columns.

@[simp]

theorem dotProduct_cons {R : Type u_1} [AddCommMonoid R] [Mul R] {n : ℕ} (a : R) (b : Vector R n) (c : R) (d : Vector R n) : (Vector.cons a b).get ⬝ᵥ (Vector.cons c d).get = a * c + b.get ⬝ᵥ d.get

theorem Vector.dotProduct_eq_root_dotProduct {R : Type u_1} [AddCommMonoid R] [Mul R] {n : ℕ} (a b : Vector R n) : a.dotProduct b = a.get ⬝ᵥ b.get

theorem Vector.map_dotProduct {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) {n : ℕ} (a b : Vector R n) : f (a.dotProduct b) = (map (⇑f) a).dotProduct (map (⇑f) b)

A ring homomorphism maps a dot product to the dot product of the mapped vectors.