A vector range

Stream: Is there code for X?

[Bolton Bailey]

Is there code for a vector range analogous to the list.range function? If not, should this be added to vector.lean?

/-- Vector form of range function -/
def vector_range (k : ℕ) : vector ℕ k :=
⟨list.range k, by simp⟩

[Yakov Pechersky]

It doesn't currently. I've played around with it for quite some bit. What do you plan to do with it? I've found that working in lists usually ended up being easier.

[Bolton Bailey]

This function was useful for me when I wanted to represent a vector of powers of a polynomial variable, which I do using the expression
def powers_of_τ : vector (mv_polynomial vars F) m := vector.map (λ i, X_poly^i) (vector_range m)
In this case I want to use vector rather than list because later I want to take the dot product of this vector with another vector of polynomials, which I do using vector.map₂ with * and then calling to_list and sum. I suppose I could convert everything to lists and use list.map₂, but this seems less clean and I think I would later need to prove that these two lists are the same length. This actually raises another point: Is there code for taking the dot product of vectors of ring elements?

[Yakov Pechersky]

Might be easier to do this in fin n \to R

[Yakov Pechersky]

Because if you're going to reason about sum, it's going to be some unwieldy thing about foldr or something like it, and you'll be juggling lemmas about associativity and identity elements. In fin n \to R, you can use all the existing big_operators lemmas about fintypes and fin.

[Bolton Bailey]

That sounds great. What are are these big_operators you are talking about? big_operators does not come up in a search of the lean documentation.

[Reid Barton]

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html