## Stream: new members

### Topic: Ones vector inner product

#### Ashley Blacquiere (Oct 06 2022 at 05:36):

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 (Oct 06 2022 at 05:54):

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

#### Eric Wieser (Oct 06 2022 at 05:55):

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

#### Matt Diamond (Oct 06 2022 at 06:08):

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

#### Junyan Xu (Oct 06 2022 at 06:09):

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

#### Ashley Blacquiere (Oct 06 2022 at 06:26):

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 (Oct 06 2022 at 07:07):

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

#### Eric Wieser (Oct 06 2022 at 07:08):

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

Last updated: Dec 20 2023 at 11:08 UTC