Zulip Chat Archive

Stream: Is there code for X?

Topic: A vector range


view this post on Zulip Bolton Bailey (Dec 02 2020 at 22:58):

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

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 23:05):

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.

view this post on Zulip Bolton Bailey (Dec 02 2020 at 23:30):

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?

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 23:31):

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

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 23:32):

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.

view this post on Zulip Bolton Bailey (Dec 03 2020 at 10:02):

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.

view this post on Zulip Reid Barton (Dec 03 2020 at 10:04):

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


Last updated: May 16 2021 at 05:21 UTC