Ones vector inner product

Stream: new members

[Ashley Blacquiere]

I'm trying to formalize the following:

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

where 1 is the all-ones vector <1, 1, ...> of length |x|

I've tried defining the all-ones vector and the inequality as follows, but I'm not sure that what I've done is doing what I think it's doing...

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

Is this sensible, or am I going off the deep-end here?

[Eric Wieser]

The all-ones vector would normally be spelt (1 : fin n → ℝ)

[Eric Wieser]

docs#vector in mathlib is only ever used in the C++ sense of the word, not the usual mathematical meaning.

[Matt Diamond]

I had no idea you could coerce a number to a function... is there anything in the docs about that?

[Junyan Xu]

I think it's the docs#pi.has_one instance

[Ashley Blacquiere]

Eric Wieser said:

The all-ones vector would normally be spelt (1 : fin n → ℝ)

Eric Wieser said:

docs#vector in mathlib is only ever used in the C++ sense of the word, not the usual mathematical meaning.

So, if I'm understanding correctly, I shouldn't really be using docs#vector in the sense above - I should be doing something more like this (barring the fact that this isn't a working example, since the types on the left of the inequality don't agree):

lemma one_vector_prod (x : F) : ⟪(1 : fin n → ℝ), x⟫_ℝ ≤ ∥(1 : fin n → ℝ)∥ * ∥x∥ := real_inner_le_norm x x

[Eric Wieser]

I suspect you actually want 1 : euclidean_space (fin n) ℝ

[Eric Wieser]

Since that has the norm structure that you want, as opposed to fin n → ℝ which has the inf-norm