Chauchy-Schwarz

Stream: Is there code for X?

[Damiano Testa]

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]

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

[Heather Macbeth]

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]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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