## Stream: Is there code for X?

### Topic: inequality lemma

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


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

#### 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?

#### Greg Price (Mar 31 2021 at 19:22):

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

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

#### Heather Macbeth (Mar 31 2021 at 19:24):

You would need docs#euclidean_space to apply it.

#### 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:

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

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

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

#### Heather Macbeth (Mar 31 2021 at 19:28):

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

#### Heather Macbeth (Mar 31 2021 at 19:29):

docs#real.inner_le_Lp_mul_Lq

#### 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?

#### Greg Price (Mar 31 2021 at 19:31):

Yeah, that sounds great.

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

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

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