Library stability

Require Import Fourier.
Require Export one_d_wave_equation.

Open Local Scope nat_scope.
Open Local Scope R_scope.

Section Stab.

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

Variable c:R.
Variable u0h u1h: R*R -> Z-> R.
Variable fh: R*R -> Z -> nat -> R.
Variable unh : R * R -> Z -> nat -> R.
Variable usol : R * R -> R.
Variable eps:R.
Variable dX:R*R.

Hypothesis unh_is_discrete_sol: is_discrete_solution xmin xmax c u0h u1h fh unh dX.
Hypothesis eps_lt: 0 < eps < 1.
Hypothesis CFL_eps: CFL_condition_r c eps dX.
Hypothesis c_pos: 0 < c.

Notation ni x := (ni xmin xmax x).
Notation finite_dot_product_dx := (fun dx u v => (finite_dot_product_dx xmin xmax dx u v)).
Notation finite_squared_norm_dx := (fun dx u => (finite_squared_norm_dx xmin xmax dx u)).
Notation finite_norm_dx := (fun dx u => (finite_norm_dx xmin xmax dx u)).
Notation energy := (fun c uh dX n => energy xmin xmax c uh dX n).

Lemma energy_increases: forall n:nat,
   0 < fst dX -> snd dX <> 0 -> (0<n)%nat->
   (energy c (unh dX) dX n) - (energy c (unh dX) dX (n-1)%nat) =
  1/2*finite_dot_product_dx (fst dX) (fun j => fh dX j n)
            (fun j => unh dX j (n+1)%nat - unh dX j (n-1)%nat).

Lemma minorationenergy: forall n,
   snd dX <> 0 -> 0 < (fst dX) ->
    1/2*(1-Rsqr (CFL c dX))*
  finite_squared_norm_dx (fst dX)
       (fun j=> 1/(snd dX)*(unh dX j (n+1)%nat - unh dX j n))
  <= energy c (unh dX) dX n.

Lemma energy_pos:
 forall n, (0 < snd dX) -> 0 < (fst dX) ->
   0 <= energy c (unh dX) dX n.


Lemma minorationenergy2:
  forall n,
  0 < fst dX -> 0 < snd dX ->
     finite_norm_dx (fst dX)
        (fun j : Z =>
          unh dX j (n+1) -
          unh dX j n) <=
   (sqrt 2 / sqrt (2*eps - Rsqr eps) * snd dX *
       sqrt (energy c (unh dX) dX n)).

Lemma energy_majoration_aux:
 forall n, (0 < n)%nat -> 0 < snd dX-> 0 < fst dX ->
  sqrt (energy c (unh dX) dX n)
   <= sqrt (energy c (unh dX) dX (n-1)%nat)
     + (sqrt 2 / (2*sqrt (2*eps-Rsqr eps)))
           * (snd dX) * (finite_norm_dx (fst dX)
                               (fun j => fh dX j n)).

Lemma energy_majoration:
 0 < snd dX-> 0 < fst dX ->
  forall t,
    let k:= (kt t (snd dX) -1)%nat in
    sqrt (energy c (unh dX) dX k)
       <= sqrt (energy c (unh dX) dX 0%nat)
               + (sqrt 2 / (2*sqrt (2*eps-Rsqr eps))) * (snd dX) * sum_f 1 k
                     (fun n => (finite_norm_dx (fst dX)
                               (fun j => fh dX j n))).

Lemma energy_majoration_zero:
 0 < snd dX-> 0 < fst dX ->
  (forall j k, fh dX j k =0) ->
  forall t,
    let k:= (kt t (snd dX) -1)%nat in
    sqrt (energy c (unh dX) dX k)
       <= sqrt (energy c (unh dX) dX 0%nat).

End Stab.