Equality criterion for Cauchy-Schwarz ineq, simple case

Stream: new members

[Ilmārs Cīrulis]

[I work for AI company right now etc., this is for olympiad math.]

I tried to find equality criterion for Cauchy-Schwarz inequality (the inequality), when it is case of sums in real numbers over Finsets.

Closest I could find was more general case with inner product and norm: docs#inner_eq_norm_mul_iff

I had difficulties using this general version to prove the simpler case I wanted. :(

Maybe someone has done it already?

[Matt Diamond]

I think this is it? docs#Finset.sum_sq_le_sum_mul_sum_of_sq_eq_mul

[Matt Diamond]

also note docs#Finset.sum_mul_sq_le_sq_mul_sq just below it

[Ilmārs Cīrulis]

This is for the inequality. It is useful (i'm using it already) but not a criterion for the case when there's equality.

[Matt Diamond]

ah okay, darn

[Ilmārs Cīrulis]

still, thank you

[Ilmārs Cīrulis]

More general version I tried to prove:

import Mathlib

lemma finset_Cauchy_Schwarz_equality_criterion {ι: Type} (s: Finset ι) (f g: ι → ℝ):
    (∑ i ∈ s, f i * g i) ^ 2 = (∑ i ∈ s, f i ^ 2) * (∑ i ∈ s, g i ^ 2) ↔
    (f = 0 ∨ g = 0 ∨ ∃ k, ∀ i ∈ s, f i = k * g i) := by sorry

Trying to prove this right now:

import Mathlib

lemma fintype_Cauchy_Schwarz_equality_criterion n (f g: Fin n → ℝ):
    (∑ i, f i * g i) ^ 2 = (∑ i, f i ^ 2) * (∑ i, g i ^ 2) ↔
    (f = 0 ∨ g = 0 ∨ ∃ k, ∀ i, f i = k * g i) := by sorry

[Luigi Massacci]

Isn't the proof almost rfl with the above docs#inner_eq_norm_mul_iff?

[Ilmārs Cīrulis]

It is. I'm trying to use the docs#inner_eq_norm_mul_iff_real (the same, but for real numbers) right now...

But stuck with almost nothing right now:

import Mathlib

lemma fintype_Cauchy_Schwarz_equality_criterion n (f g: Fin n → ℝ):
    (∑ i, f i * g i) ^ 2 = (∑ i, f i ^ 2) * (∑ i, g i ^ 2) ↔
    (f = 0 ∨ g = 0 ∨ ∃ k, ∀ i, f i = k * g i) := by
  set x: EuclideanSpace ℝ (Fin n) := (WithLp.equiv _ _).symm f
  set y: EuclideanSpace ℝ (Fin n) := (WithLp.equiv _ _).symm g
  have H := inner_eq_norm_mul_iff_real (x := x) (y := y)
  simp [x, y] at H
  sorry

[Luigi Massacci]

I think liberal use of congr should lead you to your goal fairly quickly

[Ilmārs Cīrulis]

Thank you! Will try that too.
I did quite a few unfolds with simps on the norms and it works too.

[Ilmārs Cīrulis]

My current version which works:

import Mathlib

lemma fin_Cauchy_Schwarz_equality_criterion n (f g: Fin n → ℝ):
    (∑ i, f i * g i) = √(∑ i, f i ^ 2) * √(∑ i, g i ^ 2) ↔
    (∀ i, √(∑ i, g i ^ 2) * f i = √(∑ i, f i ^ 2) * g i) := by
  set x: EuclideanSpace ℝ (Fin n) := (WithLp.equiv _ _).symm f
  set y: EuclideanSpace ℝ (Fin n) := (WithLp.equiv _ _).symm g
  have H := inner_eq_norm_mul_iff_real (x := x) (y := y)
  simp [x, y] at H
  have Ht (t: Fin n → ℝ): ‖(WithLp.equiv 2 (Fin n → ℝ)).symm t‖ = √(∑ i, (t i) ^ 2) := by
    unfold WithLp.equiv
    unfold Equiv.refl
    simp
    unfold norm
    unfold PiLp.instNorm
    simp
    have H0: 0 ≤ ∑ i, t i ^ 2 := by
      apply Finset.sum_nonneg
      intros i
      simp
      apply sq_nonneg (t i)
    refine (Real.rpow_inv_eq H0 ?_ ?_).mpr ?_
    . apply Real.sqrt_nonneg
    . norm_num
    . rw [← Real.rpow_div_two_eq_sqrt 2 H0]
      simp
  simp_rw [Ht] at H
  have H0: ∑ x, g x * f x = ∑ x, f x * g x := by
    congr
    ext x
    apply mul_comm
  rw [H0] at H
  rw [H]
  have Ht0 (k: ℝ) (t: Fin n → ℝ): k • (WithLp.equiv 2 (Fin n → ℝ)).symm t = fun x => k * t x := by
    congr
  rw [Ht0, Ht0]
  constructor <;> intro H1
  . rw [funext_iff] at H1
    exact H1
  . rw [funext_iff]
    exact H1

[Ilmārs Cīrulis]

And this too.

import Mathlib

lemma fin_Cauchy_Schwarz_equality_criterion {n} (f g: Fin n → ℝ) (Hf: f ≠ 0) (Hg: g ≠ 0):
    abs (∑ i, f i * g i) = √(∑ i, f i ^ 2) * √(∑ i, g i ^ 2) ↔
    (∃ (k: ℝ), ¬ k = 0 ∧ ∀ i, g i = k * f i) := by
  set x: EuclideanSpace ℝ (Fin n) := (WithLp.equiv _ _).symm f
  set y: EuclideanSpace ℝ (Fin n) := (WithLp.equiv _ _).symm g
  have H := norm_inner_eq_norm_iff (𝕜 := ℝ) (x := x) (y := y) Hf Hg
  simp [x, y] at H
  have Ht (t: Fin n → ℝ): ‖(WithLp.equiv 2 (Fin n → ℝ)).symm t‖ = √(∑ i, (t i) ^ 2) := by
    unfold WithLp.equiv Equiv.refl norm PiLp.instNorm
    simp
    have H0: 0 ≤ ∑ i, t i ^ 2 := by
      apply Finset.sum_nonneg
      intros i
      simp
      apply sq_nonneg (t i)
    refine (Real.rpow_inv_eq ?_ ?_ ?_).mpr ?_
    . apply Finset.sum_nonneg
      intros i
      simp
      apply sq_nonneg (t i)
    . apply Real.sqrt_nonneg
    . norm_num
    . rw [← Real.rpow_div_two_eq_sqrt 2 H0]
      simp
  simp_rw [Ht] at H
  rw [H]
  have Ht0 (k: ℝ) (t: Fin n → ℝ): k • (WithLp.equiv 2 (Fin n → ℝ)).symm t = fun x => k * t x := by
    congr
  simp_rw [Ht0]
  constructor <;> intro H1
  . obtain ⟨k, Hk, H1⟩ := H1
    rw [funext_iff] at H1
    use k
    exact ⟨Hk, H1⟩
  . obtain ⟨k, Hk, H1⟩ := H1
    use k
    rw [funext_iff]
    exact ⟨Hk, H1⟩