# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Chauchy-Schwarz

#### Damiano Testa (Feb 24 2021 at 17:45):

Dear All,

is there a proof of the Cauchy-Schwarz inequality in mathlib? Ideally, I would like a statement that also addresses the case of equality, but just the inequality for vectors in `ℝ ^ 2`

(or whatever generalized `partial_ordered`

type with a hint of `scalar_product`

) would already be great news!

#### Heather Macbeth (Feb 24 2021 at 17:46):

Yes, there's a lot, depending on the form you need!

#### Heather Macbeth (Feb 24 2021 at 17:47):

Some versions of the equality case for arbitrary inner product spaces

docs#abs_inner_div_norm_mul_norm_eq_one_iff

docs#abs_inner_eq_norm_iff

docs#inner_eq_norm_mul_iff

etc

#### Damiano Testa (Feb 24 2021 at 17:48):

Ah, cool! I would like a statement that gives me as quickly as possible that if `v w : ℤ × ℤ`

are independent, then there is a linear combination of `v w`

that has strictly positive pairing with both `v`

and `w`

.

#### Damiano Testa (Feb 24 2021 at 17:48):

Since this is to test a more general case, I do not mind if I have to tweak the hypotheses somewhat.

#### Damiano Testa (Feb 24 2021 at 17:49):

Heather, I will take a look: thank you very much!

#### Damiano Testa (Feb 24 2021 at 17:52):

Ok, it seems that `abs_real_inner_div_norm_mul_norm_le_one`

is the inequality, and the references that Heather gave deal with the extreme case: this is looking great! Thanks a lot!

#### Heather Macbeth (Feb 24 2021 at 18:05):

You will probably also need that $\mathbb{R}^n$ actually is an inner product space -- this is docs#euclidean_space.inner_product_space

#### Damiano Testa (Feb 24 2021 at 18:11):

Ah, great! I was trying to find the "standard scalar product" on R^n!

Last updated: May 16 2021 at 05:21 UTC