Cauchy-Schwarz inequality

[lowasser]

This is Theorem 78 in the 100 Theorems, and its most general setting is an inner product space, which shouldn't be terrifically difficult to define after we define real vector spaces in #1689.

[fredrik-bakke]

The Pythagorean theorem (Nr. 4) is also very naturally proved in the general setting of inner product spaces :)

[lowasser]

Not looking in detail yet, but this may be hard or may require classical axioms: in https://math.stackexchange.com/q/2905324/23995 other people seem to struggle heavily with proving Cauchy-Schwarz constructively. My first attempt failed, certainly.

[lowasser]

I have an idea that'll need fourth roots, but I think it might work. I'm mostly writing this so I remember in the morning.

[malarbol]

I may have a plan for a proof. I don't have the time to try it now but that could interest you:

First, prove the lemma for the unit ball:

∀ x , y ; if ∥x∥² ≤ 1 and ∥y∥² ≤ 1 then ∣⟨x,y⟩| ≤ 1

proof:

0 ≤ ∥x - y∥² = ∥x∥² + ∥y∥² - 2⟨x,y⟩ ≤ 2⋆(1 - ⟨x,y⟩) ⇒ ⟨x,y⟩ ≤ 1
0 ≤ ∥x + y∥² = ∥x∥² + ∥y∥² + 2⟨x,y⟩ ≤ 2⋆(1 + ⟨x,y⟩) ⇒ -⟨x,y⟩ ≤ 1

so

∣⟨x,y⟩∣ ≤ 1.

Then, for generic x and y, apply the lemma to

u = (∥x∥ + ε)⁻¹ * x
v = (∥y∥ + δ)⁻¹ * y

for any ε, δ > 0 to get

∀ ε, δ > 0; ∣⟨x,y⟩∣ ≤ ∥x∥∥y∥ + δ∥x∥ + ε∥y∥ + εδ.

Finally, ∀ η > 0 choose ε and δ such that δ∥x∥ + ε∥y∥ + εδ < η so

∀ η > 0; ∣⟨x,y⟩∣ ≤ ∥x∥∥y∥ + η

and use saturation to conclude that ∣⟨x,y⟩∣ ≤ ∥x∥∥y∥.

[lowasser]

Interesting. I had managed to get to ∥u ∙ v∥² ∥u∥² ∥v∥² ≤ ∥u∥⁴ ∥v∥⁴, but the idea of adding an epsilon had not yet occurred to me.

[lowasser]

I think the tricksy bit in that proof is in fact showing that (∥x∥ + ε)⁻¹ * x has magnitude at most 1, but I have some ideas on how to do that; if nothing else, we could bound ∥x∥ by a positive rational number and do it in the rationals where we can do casework.

[malarbol]

I think the tricksy bit in that proof is in fact showing that (∥x∥ + ε)⁻¹ * x has magnitude at most 1

Can't we use

∥x∥ < ∥x∥ + ε ⇒ ∥(∥x∥ + ε)⁻¹ * x∥ < 1 

?

[malarbol]

with

∀ λ ∈ ℝ , x ∈ V , ∥λ x∥ = ∣λ∣ ∥x∥

and λ = (∥x∥ + ε)⁻¹

[lowasser]

It took a bit of work, but I got that figured out.

[lowasser]

The missing lemma we didn't actually have was

exists-ℚ⁺-mul-le-one-ℝ⁰⁺ : {l : Level} (x : ℝ⁰⁺ l) → exists ℚ⁺ (λ q → le-prop-ℝ⁰⁺ (nonnegative-real-ℚ⁺ q *ℝ⁰⁺ x) one-ℝ⁰⁺)