Zulip Chat Archive

Stream: Is there code for X?

Topic: Chauchy-Schwarz


view this post on Zulip 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!

view this post on Zulip Heather Macbeth (Feb 24 2021 at 17:46):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 24 2021 at 17:49):

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

view this post on Zulip 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!

view this post on Zulip Heather Macbeth (Feb 24 2021 at 18:05):

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

view this post on Zulip 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