Building short sequences

Stream: new members

[Sammy Webb]

Hi I ran into some unfamiliar waters during a proof this week. As part of proving the Cauchy Schwarz Inequality I built a case for n = 2. Then to apply it in my proof I was initially having some difficulty but I found a hacky way round I am hoping to find out if there is a more standard way to solve the problem I solved.

I was trying to define some short sequences to connect my two theorems. If anyone has any advice on a better way to do this it would be greatly appreciated. Can share the code for the other version of CS inequality but its long and I didn't want to make this post overly long.

-- #check prop_3_5
lemma Cauchy_Schwarz_Inequality_2'' ( a: ℝ ) ( b: ℝ ) ( c: ℝ  )( d: ℝ ) :a * b + c * d ≤ Real.sqrt (a ^ 2 + c ^ 2) * Real.sqrt (b ^ 2 + d ^ 2) := by
  let xs : Nat → Real
  | 0   => a
  | 1   => c
  | x => x
  let ys : Nat → Real
  | 0   => b
  | 1   => d
  | y => y
  have x0 : xs 0 = a := by
    rfl
  rw [← x0]
  have x1 : xs 1 = c := by
    rfl
  rw [← x1]
  have y0 : ys 0 = b := by
    rfl
  rw [← y0]
  have y1 : ys 1 = d := by
    rfl
  rw [← y1]
  apply Cauchy_Schwarz_Inequality_2'
  --  Cauchy_Schwarz_Inequality_2' (x y : ℕ → ℝ) :
  -- x 0 * y 0 + x 1 * y 1 ≤ Real.sqrt (x 0 ^ 2 + x 1 ^ 2) * Real.sqrt (y 0 ^ 2 + y 1 ^ 2)

[Richard Copley]

No need for the rewrites:

import Mathlib.Data.Real.Sqrt

theorem Cauchy_Schwarz_Inequality_2' (x y : ℕ → ℝ) :
    x 0 * y 0 + x 1 * y 1 ≤ Real.sqrt (x 0 ^ 2 + x 1 ^ 2) * Real.sqrt (y 0 ^ 2 + y 1 ^ 2) :=
  sorry

lemma Cauchy_Schwarz_Inequality_2'' (a b c d : ℝ) :
    a * b + c * d ≤ Real.sqrt (a ^ 2 + c ^ 2) * Real.sqrt (b ^ 2 + d ^ 2) := by
  let xs : ℕ → ℝ | 0 => a | 1 => c | _ => 0
  let ys : ℕ → ℝ | 0 => b | 1 => d | _ => 0
  exact Cauchy_Schwarz_Inequality_2' xs ys

Have you seen docs#Finset.sum_mul_sq_le_sq_mul_sq and docs#sum_mul_sq_le_sq_mul_sq? [Edit: I meant docs#sum_mul_le_sqrt_mul_sqrt]

[Sammy Webb]

Thank you very much that is very helpful.

As for have I seen those, only in passing. I am formalising a university course as part of a university project so the objective is to follow the proofs given in the course as closely as I can hence why I am not using these to complete the proofs but thank you very much for sharing them with me just incase.