inequality lemma

Stream: Is there code for X?

[Manuel Candales]

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

[Kevin Buzzard]

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

[Manuel Candales]

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

[Manuel Candales]

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

[Greg Price]

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

[Heather Macbeth]

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

[Heather Macbeth]

You would need docs#euclidean_space to apply it.

[Greg Price]

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

[Bryan Gin-ge Chen]

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

[Greg Price]

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.

[Heather Macbeth]

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

[Greg Price]

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.

[Heather Macbeth]

docs#real.inner_le_Lp_mul_Lq

[Bryan Gin-ge Chen]

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?

[Greg Price]

Yeah, that sounds great.

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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.

[Scott Morrison]

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.