Library R_n

R^n

Require Export Differential.
Require Export Fourier.
Require Export Reals_compl.
Require ZArith.
Open Local Scope R_scope.

Section Rn.

Variable xmin xmax:R.
Hypothesis xminLtxmax: xmin < xmax.

Definition ni (dx:R): Z :=
  ((jx (xmax -xmin) dx))%Z.

Lemma ni_pos:
   forall dx, 0 < dx -> (0 <= ni dx)%Z.

Lemma ni_Zabs_nat: forall dx, 0 < dx ->
  Z_of_nat (Zabs_nat (ni dx)) = ni dx.

R^n is a vector space. Vectors in R^n are represented by nat -> R functions

Definition add_n (f g : Z -> R) : Z -> R :=
  fun i => f i + g i.

Definition subtract_n (f g : Z -> R) : Z -> R :=
  fun i => f i - g i.

Definition scalar_multiply_n (l : R) (f : Z -> R) : Z -> R :=
  fun i => l * f i.

Notation "f + g" := (add_n f g) : type_scope.
Notation "f - g" := (subtract_n f g) : type_scope.

Definition of the dot_product from 0 to n:nat where we add from 0 to n-1

Fixpoint dot_product_n (n:nat) (f g : Z -> R) {struct n} : R :=
  match n with
  | 0 => 0
  | S n' => (f (Z_of_nat n')) * (g (Z_of_nat n')) + dot_product_n n' f g
  end.

Definition squared_norm_n (n:nat) (f : Z -> R) := dot_product_n n f f.

Many lemmas

Lemma dot_product_n_zero :
  forall u v n,
    (forall i : Z,
        (0 <= i < Z_of_nat n)%Z -> u i = 0 \/ v i = 0) ->
    dot_product_n n u v = 0.

Lemma dot_product_n_distr_l :
  forall (n : nat) (f g h : Z -> R),
  dot_product_n n f g + dot_product_n n h g =
  dot_product_n n (add_n f h) g.

Lemma dot_product_n_distr_r :
  forall (n : nat) (f g h : Z -> R),
  dot_product_n n f g + dot_product_n n f h =
  dot_product_n n f (add_n g h).

Lemma dot_product_n_sub_distr_l :
  forall (n : nat) (f g h : Z -> R),
  dot_product_n n f g - dot_product_n n h g =
  dot_product_n n (subtract_n f h) g.

Lemma dot_product_n_sub_distr_r :
  forall (n : nat) (f g h : Z -> R),
  dot_product_n n f g - dot_product_n n f h =
  dot_product_n n f (subtract_n g h).

Lemma dot_product_n_scal_mult_l :
  forall (n : nat) (l : R) (f g : Z -> R),
  dot_product_n n (scalar_multiply_n l f) g =
  l * dot_product_n n f g.

Lemma dot_product_n_scal_mult_r :
  forall (n : nat) (l : R) (f g : Z -> R),
  dot_product_n n f (scalar_multiply_n l g) =
  l * dot_product_n n f g.

Lemma dot_product_n_sym :
  forall (n : nat) (f g : Z -> R),
  dot_product_n n f g = dot_product_n n g f.

Lemma dot_product_n_eq_suf_l :
  forall (n : nat) (f g h: Z -> R),
  (forall i, (0 <= i < Z_of_nat n)%Z -> f i = g i) ->
   dot_product_n n f h = dot_product_n n g h.

Lemma dot_product_n_eq_suf_r :
  forall (n : nat) (f g h: Z -> R),
  (forall i : Z, (0 <= i < Z_of_nat n)%Z -> f i = g i) ->
   dot_product_n n h f = dot_product_n n h g.

Lemma dot_product_n_eq_suf_strict_l :
  forall (n : nat) (f g h: Z -> R),
  (forall i, (0 < i < Z_of_nat n)%Z -> f i = g i) ->
  h 0%Z = 0 ->
   dot_product_n n f h = dot_product_n n g h.

Lemma dot_product_n_eq_suf_strict_r :
  forall (n : nat) (f g h: Z -> R),
  (forall i : Z, (0 < i < Z_of_nat n)%Z -> f i = g i) ->
  h 0%Z = 0 ->
  dot_product_n n h f = dot_product_n n h g.

Lemma dot_product_n_shift_indices: forall (n:nat) (f1 f2 : Z -> R),
  dot_product_n n f1 f2 =
        dot_product_n n (fun j => f1 (j+1)%Z) (fun j => f2 (j+1)%Z)
         + f1 0%Z*f2 0%Z - f1 (Z_of_nat n) * f2 (Z_of_nat n).

Lemma squared_norm_n_pos_aux:
  forall (n:nat) (f: Z -> R),
    0 <= (dot_product_n n f f).

Lemma squared_norm_n_pos:
  forall n (f: Z -> R),
     (0 <= squared_norm_n n f).

Lemma squared_norm_n_scal_mult_n: forall n (r:R) (f:Z -> R),
   (squared_norm_n n (scalar_multiply_n r f)) = r*r*(squared_norm_n n f).

Lemma squared_norm_n_plus: forall n (f g:Z->R),
  (squared_norm_n n (f+g)%type = squared_norm_n n f + squared_norm_n n g
  + 2 * dot_product_n n f g)%R.

Lemma squared_norm_n_majoration: forall n f M,
  (forall j, (0 <= j < Z_of_nat n)%Z -> Rsqr (f j) <= M) ->
  dot_product_n n f f <= INR n * M.

Lemma Cauchy_Schwarz: forall n f1 f2,
   Rabs (dot_product_n n f1 f2)
      <= sqrt (squared_norm_n n f1) * sqrt (squared_norm_n n f2).

Definition finite_dot_product_dx dx u v := dx*dot_product_n (Zabs_nat (ni dx)) u v.

Definition finite_squared_norm_dx dx u := finite_dot_product_dx dx u u.

Definition finite_norm_dx dx u := sqrt (finite_squared_norm_dx dx u).

Lemmas about the finite dot product

Lemma finite_dot_product_dx_zero1:
  forall dx f g, 0 < dx ->
  (forall i, (0 <= i < ni dx)%Z -> f i = 0) ->
  finite_dot_product_dx dx f g = 0.

Lemma finite_dot_product_dx_zero1ou2:
  forall dx f g, 0 < dx ->
  (forall i, (0 <= i < ni dx)%Z -> f i = 0 \/ g i =0) ->
  finite_dot_product_dx dx f g = 0.

Lemma finite_squared_norm_dx_pos: forall dx f,
  (0 <= dx) ->
   0 <= finite_squared_norm_dx dx f.

Lemma finite_squared_norm_dx_eq: forall dx f1 f2, 0 < dx ->
  (forall i, (0 <= i < ni dx)%Z -> f1 i = f2 i) ->
  finite_squared_norm_dx dx f1 = finite_squared_norm_dx dx f2.

Lemma finite_squared_norm_dx_zero: forall dx f, 0 < dx ->
   (forall i, (0 <= i < ni dx)%Z -> f i = 0) ->
  finite_squared_norm_dx dx f = 0.

Lemma finite_squared_norm_dx_homogen: forall dx l f,
  finite_squared_norm_dx dx (scalar_multiply_n l f) =
    l * l * finite_squared_norm_dx dx f.

Lemma finite_Cauchy_Schwarz_dx: forall dx f1 f2,
   0 <= dx ->
   Rabs (finite_dot_product_dx dx f1 f2)
      <= finite_norm_dx dx f1 * finite_norm_dx dx f2.

Lemma finite_squared_norm_dx_triang: forall dx f1 f2,
  0 <= dx ->
  finite_norm_dx dx (fun j => f1 j + f2 j) <=
      finite_norm_dx dx f1 + finite_norm_dx dx f2.

Lemma finite_squared_norm_dx_majoration: forall dx f M,
   0 < dx -> 0 <= M ->
   (forall j : Z, (0 <= j < ni dx )%Z -> Rsqr (f j) <= M) ->
   finite_squared_norm_dx dx f <= (xmax -xmin ) * M.

Lemma finite_dot_product_dx_sym: forall dx u v,
   finite_dot_product_dx dx u v = finite_dot_product_dx dx v u.

Lemma finite_dot_product_dx_eq_l: forall dx u v w, 0 < dx ->
   (forall i, (0 <= i < ni dx)%Z -> u i = v i) ->
   finite_dot_product_dx dx u w = finite_dot_product_dx dx v w.

Lemma finite_dot_product_dx_eq_r: forall dx u v w, 0 < dx ->
   (forall i, (0 <= i < ni dx)%Z -> u i = v i) ->
   finite_dot_product_dx dx w u = finite_dot_product_dx dx w v.

Lemma finite_dot_product_dx_eq_strict_l: forall dx u v w, 0 < dx ->
   (forall i, (0 < i < ni dx)%Z -> u i = v i) ->
   w 0%Z = 0 ->
   finite_dot_product_dx dx u w = finite_dot_product_dx dx v w.

Lemma finite_dot_product_dx_eq_strict_r: forall dx u v w, 0 < dx ->
   (forall i, (0 < i < ni dx)%Z -> u i = v i) ->
   w 0%Z = 0 ->
   finite_dot_product_dx dx w u = finite_dot_product_dx dx w v.

Lemma finite_dot_product_dx_add_l: forall dx u v w,
   finite_dot_product_dx dx (add_n u v) w=
   finite_dot_product_dx dx u w + finite_dot_product_dx dx v w.

Lemma finite_dot_product_dx_add_r: forall dx u v w,
   finite_dot_product_dx dx w (add_n u v) =
   finite_dot_product_dx dx w u + finite_dot_product_dx dx w v.

Lemma finite_dot_product_dx_sub_l: forall dx u v w,
   finite_dot_product_dx dx (subtract_n u v) w =
   finite_dot_product_dx dx u w - finite_dot_product_dx dx v w.

Lemma finite_dot_product_dx_sub_r: forall dx u v w,
   finite_dot_product_dx dx w (subtract_n u v) =
   finite_dot_product_dx dx w u - finite_dot_product_dx dx w v.

Lemma finite_dot_product_dx_scal_mult_l :
  forall dx u v l,
  finite_dot_product_dx dx (scalar_multiply_n l u) v =
  l * finite_dot_product_dx dx u v.

Lemma finite_dot_product_dx_scal_mult_r :
  forall dx u v l,
  finite_dot_product_dx dx u (scalar_multiply_n l v) =
  l * finite_dot_product_dx dx u v.

Lemma finite_dot_product_dx_shift_indices: forall dx (f1 f2 : Z -> R),
  0 < dx ->
  f1 0%Z = 0 \/ f2 0%Z = 0 ->
  f1 (ni dx) = 0 \/ f2 (ni dx) = 0 ->
  finite_dot_product_dx dx f1 f2 =
        finite_dot_product_dx dx (fun j => f1 (j+1)%Z) (fun j => f2 (j+1)%Z).

Lemma semi_finite_dot_product_dx: forall dx Ah u v,
  (forall u v, 0 < dx -> u 0%Z = 0 -> u (ni dx) = 0 -> v 0%Z = 0 -> v (ni dx) = 0 ->
    finite_dot_product_dx dx (Ah u) v
   = finite_dot_product_dx dx u (Ah v)) ->
  0 < dx -> u 0%Z = 0 -> u (ni dx) = 0 -> v 0%Z = 0 -> v (ni dx) = 0 ->
  finite_dot_product_dx dx (Ah u) v =
    /4 * finite_dot_product_dx dx (Ah (add_n u v)) (add_n u v)
   - /4 * finite_dot_product_dx dx (Ah (subtract_n u v)) (subtract_n u v).

Lemma finite_squared_norm_parall: forall dx x y,
finite_squared_norm_dx dx (x+y)%type +
  finite_squared_norm_dx dx (x-y)%type =
   2*(finite_squared_norm_dx dx x + finite_squared_norm_dx dx y).

Lemma finite_squared_norm_parall_add: forall dx x y,
   0 <= dx ->
   finite_squared_norm_dx dx (x+y)%type <=
  2*(finite_squared_norm_dx dx x + finite_squared_norm_dx dx y).

Lemma finite_squared_norm_parall_sub: forall dx x y,
   0 <= dx ->
   finite_squared_norm_dx dx (x-y)%type <=
  2*(finite_squared_norm_dx dx x + finite_squared_norm_dx dx y).

Lemma dot_product_n_le: forall n uh vh r1 r2,
  (forall i, (0 <= i < Z_of_nat n)%Z -> Rabs (uh i) <= r1) ->
  (forall i, (0 <= i < Z_of_nat n)%Z -> Rabs (vh i) <= r2) ->
  Rabs (dot_product_n n uh vh) <= INR n*r1*r2.

Lemma dot_product_n_le2: forall n uh vh r1 r2,
  0 <= r1 -> 0 <= r2 ->
  (forall i, (0 <= i < Z_of_nat n)%Z -> Rabs (uh i) <= r1 \/ vh i=0) ->
  (forall i, (0 <= i < Z_of_nat n)%Z -> Rabs (vh i) <= r2 \/ uh i=0) ->
  Rabs (dot_product_n n uh vh) <= INR n*r1*r2.

Lemma finite_dot_product_le: forall dx uh vh r1 r2, 0 < dx ->
  ((0 < ni dx)%Z \/ (0 <= r1 /\ 0 <= r2)) ->
  (forall i, (0 <= i < ni dx )%Z -> Rabs (uh i) <= r1) ->
  (forall i, (0 <= i < ni dx )%Z -> Rabs (vh i) <= r2) ->
  Rabs (finite_dot_product_dx dx uh vh) <= (xmax -xmin )*r1*r2.

Lemma finite_dot_product_le2: forall dx uh vh r1 r2, 0 < dx ->
  0 <= r1 -> 0 <= r2 ->
  (forall i, (0 <= i < ni dx )%Z -> Rabs (uh i) <= r1 \/ vh i=0) ->
  (forall i, (0 <= i < ni dx )%Z -> Rabs (vh i) <= r2 \/ uh i=0) ->
  Rabs (finite_dot_product_dx dx uh vh) <= (xmax -xmin )*r1*r2.

Lemma finite_norm_le: forall dx uh r, 0 < dx -> ((0 < ni dx)%Z \/ (0 <= r)) ->
  (forall i, (0 <= i < ni dx )%Z -> Rabs (uh i) <= r) ->
     finite_norm_dx dx uh <= sqrt (xmax -xmin)*r.

Lemma dot_product_n_le_reverse: forall n uh i, (0 <= i < Z_of_nat n)%Z ->
   Rsqr (uh i) <= dot_product_n n uh uh.

Lemma finite_norm_le_reverse: forall dx uh r, 0 < dx ->
    finite_norm_dx dx uh <= r -> forall i, (0 <= i < ni dx)%Z -> Rabs (uh i) <= r / sqrt (dx).

End Rn.