Cauchy-Schwarz inequality

[lowasser]

Completes #1690. Builds on #1705.

[fredrik-bakke]

Please remember that the Cauchy–Schwarz inequality is also a Wikipedia theorem
https://www.wikidata.org/wiki/Q190546

[fredrik-bakke]

Seeing as @malarbol provided the proof strategy for the main theorem here, it seems reasonable to me to award him co-authorship, both of the PR, and the 100-theorems and Wikipedia theorem entries. Is this something you have discussed? I don't want to meddle in your affairs if this is settled, of course.

[malarbol]

Seeing as @malarbol provided the proof strategy for the main theorem here, it seems reasonable to me to award him co-authorship, both of the PR, and the 100-theorems and Wikipedia theorem entries. Is this something you have discussed? I don't want to meddle in your affairs if this is settled, of course.

We haven't discussed it and I'd be glad to be mentioned as co-author. All other proofs mentioned in #1690 are basically the same:

1. Prove it for unitary vectors with the Pythagorean theorem;
2. Apply this to x * ∥x∥⁻¹ and y * ∥y∥⁻¹;
3. Use algebraic manipulation / handle special cases ∥x∥ = 0 or ∥y∥ = 0.

In our case, we don't have the disjunction ∥x∥ = 0 or ∥x∥ > 0 and we can't divide by ∥x∥⁻¹. Hence the idea to divide by ∥x∥ + ε and see where we could go from there.

For the records, I believe the same trick can be used to define some form of polar decomposition in Banach spaces: for any vector x in a Banach space, the map ε ↦ (∥x∥ + ε)⁻¹ * x defines a Cauchy approximation that converges to a unitary vector u such that u = ∥x∥ * x, I think.

[fredrik-bakke]

Suggested change

	**Author:** [Louis Wasserman](https://github.com/lowasser)
	**Author:** [malarbol](http://www.github.com/malarbol)
	**Author:** [Louis Wasserman](https://github.com/lowasser) and [malarbol](http://www.github.com/malarbol)

[fredrik-bakke]

Suggested change

	**Author:** [Louis Wasserman](https://github.com/lowasser)
	**Author:** [malarbol](http://www.github.com/malarbol)
	**Author:** [Louis Wasserman](https://github.com/lowasser) and [malarbol](http://www.github.com/malarbol)

[fredrik-bakke]

this lemma should be registered separately

[fredrik-bakke]

Suggested change

	This file describes properties of
	On this page we describe properties of