Cauchy-Schwarz inequality

Stream: new members

[Kunhao Zheng]

Hello! I'm stuck on proving an example of Cauchy-Schwarz Inequality in the case of $ \mathbb{R}^2 $.

I notice that there are a bunch of theorems at hand, but they are all talking about element about inner_product_space. For example real_inner_mul_inner_self_le that I want to use here, it talks about 2 variables of type F, but I don't know how to instantiate variables of such type.

I would like to know if there is a way to instantiate 2 variables of type F that fit in well in real_inner_mul_inner_self_le and apply it, without modifying my statement here? Any hint welcome!

import data.real.basic
import analysis.normed_space.inner_product

example (x y : ℝ) :
  (2 * x + 3 * y)^2 ≤ 13 * (x^2 + y^2) :=
begin
  sorry
end

[Eric Wieser]

So you need to pick F by deciding how you want your inner product to be defined

[Eric Wieser]

At a guess you want docs#euclidean_space, so F is euclidean_space ℝ 2

[Eric Wieser]

Which would make your statement something like

example (p : euclidean_space ℝ 2) :
  (2 * p 0 + 3 * p 1)^2 ≤ 13 * (p 0^2 + p 1^2) := sorry

which then is the same as

example (p : euclidean_space ℝ 2) :
(inner ![2, 3] p)^2 ≤ 13 * inner p p := sorry

Note I'm not suggesting you adjust your statement here, just suggesting some other statements you could prove first in order to prove your statement

[Kunhao Zheng]

Thanks! I'll give it a try

[Kunhao Zheng]

I have to change 2 to (fin 2) to make lean happy in the first statement. But the second one it complains about has_inner ℕ (euclidean_space ℝ (fin 2)) has_inner ℕ (fin 1.succ → ℕ), maybe I need to add extra info like [inner_product_space ℝ p]?

import data.real.basic
import analysis.normed_space.inner_product
import analysis.normed_space.pi_Lp

theorem algebra_cauchy2_2xp3ysqleq13txsqpysq
  (x y : ℝ) :
  (2 * x + 3 * y)^2 ≤ 13 * (x^2 + y^2) :=
begin
  -- let F:= euclidean_space ℝ (fin 2),
  -- have h₀ := @real_inner_mul_inner_self_le (euclidean_space ℝ (fin 2)) _ _ _,
  sorry
end

example (p : euclidean_space ℝ (fin 2)) :
  (2 * p 0 + 3 * p 1)^2 ≤ 13 * (p 0^2 + p 1^2) := sorry

example (p : euclidean_space ℝ (fin 2)) :
(inner ![2, 3] p)^2 ≤ 13 * inner p p := sorry

[Eric Wieser]

Lean is inferring the wrong type for ![2, 3]

[Eric Wieser]

(![2, 3] : euclidean_space ℝ (fin 2)) might be enough

[Eric Wieser]

Once the lean web editor loads for me, I can try to debug

[Eric Wieser]

import data.real.basic
import analysis.normed_space.inner_product
import analysis.normed_space.pi_Lp

theorem algebra_cauchy2_2xp3ysqleq13txsqpysq
  (x y : ℝ) :
  (2 * x + 3 * y)^2 ≤ 13 * (x^2 + y^2) :=
begin
  let v : euclidean_space ℝ (fin 2) := ![(2 : ℝ), 3],
  let w : euclidean_space ℝ (fin 2) := ![x, y],
  have h₀ := real_inner_mul_inner_self_le v w,
  simp [v, w, fin.sum_univ_succ, ←pow_two] at h₀,
  sorry
end

[Eric Wieser]

By using the let I was able to force lean to infer the types correctly without using @

[Eric Wieser]

The goal is trivial from the sorry, the key lemma you need to undo the mess made by euclidean_space is docs#fin.sum_univ_succ

[Eric Wieser]

If you remove it from the simp you'll see why

[Kunhao Zheng]

@Eric Wieser Thanks! That looks pretty nice!

import analysis.normed_space.inner_product
import analysis.normed_space.pi_Lp

theorem algebra_cauchy2_2xp3ysqleq13txsqpysq
  (x y : ℝ) :
  (2 * x + 3 * y)^2 ≤ 13 * (x^2 + y^2) :=
begin
  let v : euclidean_space ℝ (fin 2) := ![(2 : ℝ), 3],
  let w : euclidean_space ℝ (fin 2) := ![x, y],
  have h₀ := real_inner_mul_inner_self_le v w,
  simp [v, w, fin.sum_univ_succ, ←pow_two] at h₀,
  nlinarith,
end

Btw where can I find the construction syntax of ![x, y]? It seems that it is not in euclidean_space

[Ruben Van de Velde]

https://leanprover-community.github.io/mathlib_docs/data/matrix/notation.html

[Joseph Myers]

We have specializations of AM-GM to two, three or four variables in mathlib, we should probably add such specializations of Cauchy-Schwarz to specific small numbers of real variables as well, for convenience when you want to use it with a few concrete expressions rather than having an inner product space.