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.

[Alexander Comerford]

I'm new to lean and wanted to start contributing to mathlib with simple proofs from linear algebra.

I saw there was no direct proof of Cauchy-Schwarz on inner product spaces so I thought I would start there.

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.NormedSpace.Basic

variable (F : Type) [LinearOrder F] [NormedAddCommGroup F] [InnerProductSpace ℝ F]

open RealInnerProductSpace

theorem cauchy_schwarz_inequality (u v : F) :
  |⟪u, v⟫| ^ 2 ≤ ⟪u, u⟫ * ⟪v, v⟫ := by {
    simp
    -- create new variable t, and use it to rewrite hh
    let t := ⟪u, v⟫ / ⟪v, v⟫
    have hh : 0 ≤ ⟪u - t • v, u - t • v⟫ := real_inner_self_nonneg
    rw [
      inner_sub_left, inner_sub_right, inner_smul_right, inner_sub_right,
      inner_smul_right, real_inner_smul_left, real_inner_smul_left, real_inner_comm u v
    ] at hh

    -- reduce hh to 0 ≤ inner u u - inner u v ^ 2 * (inner v v)⁻¹
    ring_nf at hh; simp at hh
    rw [mul_assoc, <- inv_pow, pow_two, pow_two, <- pow_two, mul_comm, <- mul_assoc] at hh
    field_simp at hh; ring_nf at hh

    -- handle the case where v is zero
    by_cases hv_iszero : v = 0
    simp [hv_iszero]
    push_neg at hv_iszero

    -- handle the case where v is negative / positive
    cases' lt_or_gt_of_ne hv_iszero with hv_neg hv_pos

    -- handle the case where v < 0
    have hv_nonneg : 0 ≤ ⟪v, v⟫ := real_inner_self_nonneg
    obtain hv_pos | hv_zero := lt_or_eq_of_le hv_nonneg
    have hhh := mul_le_mul_of_nonneg_left hh (le_of_lt hv_pos)
    simp [mul_sub, mul_comm _ (⟪v, v⟫)⁻¹, mul_inv_cancel_left₀ (ne_of_gt hv_pos), mul_comm] at hhh
    assumption

    -- handle the case where inner v v = 0
    rw [eq_comm, inner_self_eq_zero] at hv_zero
    contradiction

    -- handle the case where v > 0
    have hv_nonneg : 0 ≤ ⟪v, v⟫ := real_inner_self_nonneg
    obtain hv_inner_neg | hv_inner_zero := lt_or_eq_of_le hv_nonneg
    have hhh := mul_le_mul_of_nonneg_left hh (le_of_lt hv_inner_neg)
    simp [mul_sub, mul_comm _ (⟪v, v⟫)⁻¹, mul_inv_cancel_left₀ (ne_of_gt hv_inner_neg), mul_comm] at hhh
    assumption

    -- handle the case where inner v v = 0
    rw [eq_comm, inner_self_eq_zero] at hv_inner_zero
    contradiction
  }

https://gist.github.com/cmrfrd/61c576ed92bd1b82901c8bf3a629cfed

Is this something that would get accepted into mathlib?

[Jireh Loreaux]

We have the Cauchy-Schwarz inequality in Mathlib.

[Jireh Loreaux]

docs#norm_inner_le_norm

[Alexander Comerford]

Jireh Loreaux said:

We have the Cauchy-Schwarz inequality in Mathlib.

I see! missed it. Thank you

[Jireh Loreaux]

Also, I highly doubt you want to assume LinearOrder F. That will basically restrict your version to hold only for F := ℝ.

[Jireh Loreaux]

This is how I would search for a named theorem in Mathlib generally: https://leansearch.net/?q=cauchy%20schwarz%20inequality

[Alexander Comerford]

Jireh Loreaux said:

Also, I highly doubt you want to assume LinearOrder F. That will basically restrict your version to hold only for F := ℝ.

Yes that was the next adaptation, although I wasn't sure how to structure the single proof for real and complex together

[Jireh Loreaux]

We have a class called docs#RCLike for this.

[Jireh Loreaux]

So, to make a field which is (morally) either ℝ or ℂ, you would write {𝕜 : Type*} [RCLike 𝕜].

[Jireh Loreaux]

but note also your assumption was about F (!!) which is the vector space, not the scalar field.

[Jireh Loreaux]

My point is that your theorem isn't even applicable to EuclideanSpace ℝ n for this reason.

[Alexander Comerford]

Jireh Loreaux said:

My point is that your theorem isn't even applicable to EuclideanSpace ℝ n for this reason.

I see, but how does RCLike connect with EuclideanSpace?

[Alexander Comerford]

Oh i see here.

EuclidianSpace is of type 𝕜 which is an RCLike

[Alexander Comerford]

Jireh Loreaux said:

but note also your assumption was about F (!!) which is the vector space, not the scalar field.

I'm not sure what you mean here. I am under the assumption that u and v in this proof are elements of the vector space and not vector spaces themselves.

you would write {𝕜 : Type*} [RCLike 𝕜].

Is this then the 'right' way to write a vector space that is RCLike?

variable {F : Type*} [IsROrC 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]

[Jireh Loreaux]

What I meant before is that this line of yours:

variable (F : Type) [LinearOrder F] [NormedAddCommGroup F] [InnerProductSpace ℝ F]

while it does make F into an inner product space over ℝ, it also assumes that F itself (not the scalar field ℝ) is linearly ordered. My point was that pretty much the only thing which is linearly ordered and an inner product space over ℝ is ℝ itself. So there was no "generality" in your original statement because of this [LinearOrder F] hypothesis.