# Zulip Chat Archive

## 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