
(** {1 Lagrange Identity, Cauchy-Schwarz and Triangle Inequalities} *)

theory LagrangeInequality

(*

sum_squares a  \times sum_squares b = (scalar product a.b)^2 +

sum {1 <= i <j <=n} (a_i b_j - a_j b_i)^2
*)

  use real.Real
  use real.Square

  (** dot product, a.k.a. scalar product, of two vectors *)
  function dot (x1:real) (x2:real) (y1:real) (y2:real) : real =
     x1*y1 + x2*y2

  (** square of the norm of a vector *)
  function norm2 (x1:real) (x2:real) : real =
     sqr x1 + sqr x2

  (** square of the norm is non-negative *)
  lemma norm2_pos :
     forall x1 x2:real. norm2 x1 x2 >= 0.0


  lemma Lagrange :
    forall a1 a2 b1 b2 : real .
       norm2 a1 a2 * norm2 b1 b2 = sqr (dot a1 a2 b1 b2) + sqr (a1 * b2 - a2 * b1)

end


theory CauchySchwarzInequality


  use real.Real
  use real.Square
  use LagrangeInequality

  lemma CauchySchwarz_aux:
     forall x1 x2 y1 y2 : real.
        sqr (dot x1 x2 y1 y2) <= norm2 x1 x2 * norm2 y1 y2

  (** norm of a vector *)
  function norm (x1:real) (x2:real) : real = sqrt (norm2 x1 x2)

  (** norm is non-negative *)
  lemma norm_pos :
     forall x1 x2:real. norm x1 x2 >= 0.0

  (** 2 lemmas to help the next one *)
  lemma sqr_le_sqrt :
    forall x y:real. sqr x <= y -> x <= sqrt y

  lemma CauchySchwarz:
     forall x1 x2 y1 y2 : real.
        dot x1 x2 y1 y2 <= norm x1 x2 * norm y1 y2

end


theory TriangleInequality

  use real.Real
  use real.Square
  use LagrangeInequality
  use CauchySchwarzInequality

(** Triangle inequality, proved thanks to
  ||x+y||² = ||x||² + 2<x,y> + ||y||²
           <= ||x||² + 2||x||*||y|| + ||y||²
           = (||x|| + ||y||)²
*)

  lemma triangle_aux :
    forall x1 x2 y1 y2 : real.
      norm2 (x1+y1) (x2+y2) <= sqr (norm x1 x2 + norm y1 y2)

  (* lemma to help the next one *)
  lemma sqr_sqrt_le :
    forall x y:real. 0.0 <= y /\ 0.0 <= x <= sqr y -> sqrt x <= y

  lemma triangle :
    forall x1 x2 y1 y2 : real.
      norm (x1+y1) (x2+y2) <= norm x1 x2 + norm y1 y2

end