Zulip Chat Archive

Stream: Is there code for X?

Topic: inequality lemma


view this post on Zulip Manuel Candales (Mar 31 2021 at 19:04):

Is this lemma in mathlib already? And if not, how should I call it?

lemma known_lemma (x y z : ) : x^2 + y^2 + z^2 - y*z - z*x - x*y  0 :=
begin
  calc  x^2 + y^2 + z^2 - y*z - z*x - x*y
      = 1/2 * ( (x - y)^2 + (y - z)^2 + (z - x)^2 ) : by ring
  ...  0 : by linarith [pow_two_nonneg (x-y), pow_two_nonneg (y-z), pow_two_nonneg (z-x)],
end

view this post on Zulip Kevin Buzzard (Mar 31 2021 at 19:07):

It also follows from Cauchy Schwarz applied to the vectors (x,y,z) and (y,z,x).

view this post on Zulip Manuel Candales (Mar 31 2021 at 19:10):

Where is Cauchy Schwarz? In general, how can I search for a theorem? Like, how do I search for Pythagoras?

view this post on Zulip Manuel Candales (Mar 31 2021 at 19:16):

Found it: https://leanprover-community.github.io/100.html

view this post on Zulip Greg Price (Mar 31 2021 at 19:22):

https://en.wikipedia.org/wiki/Cauchy–Schwarz_inequality

view this post on Zulip Heather Macbeth (Mar 31 2021 at 19:23):

Cauchy-Schwarz lives in
https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/inner_product.html
there are a variety of versions, eg, docs#real_inner_mul_inner_self_le

view this post on Zulip Heather Macbeth (Mar 31 2021 at 19:24):

You would need docs#euclidean_space to apply it.

view this post on Zulip Greg Price (Mar 31 2021 at 19:24):

The search built into the mathlib docs site seems to only look at the names, and the name "Cauchy-Schwarz" only appears in the docstrings. But a Google site: search is effective:
https://www.google.com/search?q=site:https://leanprover-community.github.io+cauchy+schwarz

where the first result is
https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/inner_product.html

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 19:26):

The search box on each page of our online docs has two different functions, which is a bit confusing. First, if you type in something in the box, after some time, a dropdown will appear with links to matching declaration names. This isn't a good way to search for named results, due to mathlib's naming conventions (though once you're familiar with those conventions, it can be an efficient way of finding what's in the library!).

Second, if instead of clicking on the links in the dropdown, you click the "Search" button, this will take you to a custom google search on the docs page. This will search all the doc strings and module docs; these are more likely to have the names you're looking for. Case in point: For if you type in "pythagorean", the dropdown is filled with stuff named pythagorean_triple; however, if you search with the Search button, there are only two results; the second of which links to analysis.normed_space.inner_product.

We should probably make all this more clear on the docs site...

view this post on Zulip Greg Price (Mar 31 2021 at 19:27):

Bryan Gin-ge Chen said:

Second, if instead of clicking on the links in the dropdown, you click the "Search" button, this will take you to a custom google search on the docs page.

Ah, good to know! In fact that does exactly (and more conveniently) the thing I suggested doing above.

view this post on Zulip Heather Macbeth (Mar 31 2021 at 19:28):

You could also prove it using Holder: let v=(a,b,c)v=(a,b,c), w=(b,c,a)w=(b, c,a), then v,wvw\langle v, w\rangle\le \lVert v\rVert \lVert w\rVert.

view this post on Zulip Greg Price (Mar 31 2021 at 19:29):

I agree that it'd be great to make that more clear somehow. The dropdown is great, but it'd apparently led me to never try actually hitting the "search" button -- I figured it would do fundamentally the same thing.

view this post on Zulip Heather Macbeth (Mar 31 2021 at 19:29):

docs#real.inner_le_Lp_mul_Lq

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 19:31):

Greg Price said:

I agree that it'd be great to make that more clear somehow. The dropdown is great, but it'd apparently led me to never try actually hitting the "search" button -- I figured it would do fundamentally the same thing.

Would making the button read "Google site search" (or something along those lines) be good enough?

view this post on Zulip Greg Price (Mar 31 2021 at 19:31):

Yeah, that sounds great.

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2021 at 19:34):

OK, I've pushed a commit. The site should hopefully be updated in 15 minutes or so.

view this post on Zulip Kevin Buzzard (Mar 31 2021 at 21:07):

If you have mathlib up and running in VS Code then searching for Cauchy Schwarz should hopefully find it because it should be a tag in the relevant file.

view this post on Zulip Scott Morrison (Mar 31 2021 at 23:38):

Yes -- Kevin's suggestion is my first method to find anything: use the builtin search in VSCode, with the mathlib repository open. Turning on regular expressions in search is usually a good idea, as then you can try keyword1.*keyword2 to find occurrences of two different things in the same place.


Last updated: May 19 2021 at 02:10 UTC