Library R_two

R^2, with basic operations and norm

Require Export Reals.
Require Export Reals_compl.
Open Local Scope nat_scope.
Open Local Scope R_scope.

R^2 is a vector space.

Definition add2 (X1 X2 : R * R) : R * R :=
  (fst X1 + fst X2, snd X1 + snd X2).

Definition subtract2 (X1 X2 : R * R) : R * R :=
  (fst X1 - fst X2, snd X1 - snd X2).

Definition scalar_multiply2 (l : R) (X : R * R) : R * R :=
  (l * fst X, l * snd X).

Notation "f + g" := (add2 f g) : type_scope.
Notation "f - g" := (subtract2 f g) : type_scope.

R^2 is an Euclidean space.

Definition norm_l2 (X : R * R) : R :=
  sqrt (Rsqr (fst X) + Rsqr (snd X)).

Lemma norm_l2_pos :
  forall X : R * R,
  0 <= norm_l2 X.

Lemma norm_l2_scalar_mult: forall X l,
  norm_l2 (scalar_multiply2 l X) = Rabs l*norm_l2 X.

Lemma norm_l2_pos_strict :
  forall X : R * R,
  ~(X = (0,0)) -> 0 < norm_l2 X.

Lemma norm_l2_proj1 :
  forall x : R,
  norm_l2 (x,0) = Rabs x.

Lemma norm_l2_proj2 :
  forall y : R,
  norm_l2 (0,y) = Rabs y.

Lemma Rabs_fst_le_norm_l2: forall X,
  Rabs (fst X) <= norm_l2 X.

Lemma Rabs_snd_le_norm_l2: forall X,
  Rabs (snd X) <= norm_l2 X.

Functions from R^2 to R.

Section defs.
Variable A B:Type.

Definition add2_fun (f g : R * R -> R) : R * R -> R :=
  fun X : R * R => f X + g X.

Definition subtract2_fun (f g : R * R -> R) : R * R -> R :=
  fun X : R * R => f X - g X.

Definition scalar_multiplyA_fun (l : R) (f : A -> R) : A -> R :=
  fun X : A => l * f X.

Definition multiply2_fun (f g : R * R -> R) : R * R -> R :=
  fun X : R * R => f X * g X.

Definition divide2_fun (f g : R * R -> R) : R * R -> R :=
  fun X : R * R => f X / g X.

Definition scalar_multiplyAA_fun (l:R) (f:A->B->R) :A->B->R :=
  fun X Y=> l*f X Y.

End defs.