Vector or something else?

Stream: new members

[Ashley Blacquiere]

This seems incredibly elementary (but so does the irrationality of sqrt 2 :joy:), but I'm finding myself going around in unending circles. I'm trying to figure out the best way to state something like the following:

∥x∥₁ = ⟨1,∣x∣⟩ ≤ ∥1∥₂ ⬝ ∥x∥₂ = √n∥x∥₂

where 1 is the all-ones vector <1, 1, ...> of length |x| and ⟨1,∣x∣⟩ is the standard inner product. I've tried to do something like this:

import analysis.inner_product_space.basic

def ones_vector (l : ℕ) : vector ℝ l := vector.repeat 1 l

lemma one_vector_prod (n : ℕ) (x : vector ℝ n) [inner_product_space ℝ (vector ℝ n)]: ⟪ones_vector n, x⟫_ℝ ≤ ∥ones_vector n∥ * ∥x∥ := real_inner_le_norm (ones_vector n) x

but I kinda feel like this isn't even really doing what I think it's doing.

Is this remotely the right direction to formalize something of the form in the first code block? For context, this is basically the first baby steps of what is intended to be a formalization of the Leftover hash lemma following Regev's proof (in claim 5.3).

[Moritz Doll]

you don't want to use vector, but the space l -> ℝ and if you want to use the norms, there is docs#pi_Lp to get different $L^p$-norms.

[Moritz Doll]

see https://leanprover-community.github.io/mathlib_docs/analysis/inner_product_space/pi_L2.html for the stuff about the inner product space

[Wrenna Robson]

vector is nearly never the correct choice, sadly.

[Ashley Blacquiere]

Well, this is embarrassing... These responses seemed familiar, which led me to realize that I had basically already asked this question and had some useful responses (with apologies to @Eric Wieser if you happened to notice that I asked twice - I wasn't ignoring your suggestions - I just forgot! :sweat_smile:). I guess that's what I get for dipping in and out of my Lean project with very little regularity...

@Wrenna Robson I've seen a couple of your other posts related to L1 norm, so maybe you can help me out: I'm trying to figure out how to relate the standard Manhattan distance L1 norm to an inner product, as the first equality in this statement:

∥x∥₁ = ⟨1,∣x∣⟩ ≤ ∥1∥₂ ⬝ ∥x∥₂ = √n∥x∥₂

I've looked at docs#pi_Lp, but it seems to go further than I need? Perhaps I need to do something like what pi_Lp.norm_eq_of_L2 is doing?