Library convergence

Require Export stability.
Require Export consistency.
Open Local Scope nat_scope.
Open Local Scope R_scope.

Section Conv.
Variable xmin xmax T:R.
Hypothesis xminLtxmax: xmin < xmax.
Hypothesis T_pos: 0 < T.

Variable partial_derive_firstvar: (R * R -> R) -> (R * R -> R).
Variable partial_derive_secondvar: (R * R -> R) -> (R * R -> R).

Variable c:R.
Variable usol : R * R -> R.
Variable u0 u1: R->R.
Variable f : R*R -> R.
Variable unh : R * R -> Z -> nat -> R.
Variable eps:R.

Let u0h := (fun dX j => u0 (fst (Xjk xmin dX j 0))).
Let u1h := (fun dX j => u1 (fst (Xjk xmin dX j 1))).
Let fh := (fun dX j k => f (Xjk xmin dX j k)).

Hypothesis usol_is_sol: is_solution xmin xmax partial_derive_firstvar partial_derive_secondvar c u0 u1 f usol.
Hypothesis unh_is_discrete_sol: forall dX, is_discrete_solution xmin xmax c u0h u1h fh unh dX.

Hypothesis f_is_zero_at_beginning: forall x, f (x,0) = 0.

Hypothesis c_pos: 0 < c.
Hypothesis eps_lt: 0 < eps < 1.

Notation Oupse := (OuP (fun dX => 0 < fst dX /\ 0 < snd dX /\ ni_exact xmin xmax dX)).
Notation OupsCFLe := (OuP (fun dX => 0 < fst dX /\ 0 < snd dX /\ CFL_condition_r c eps dX /\ ni_exact xmin xmax dX)).

Notation ni x := (ni xmin xmax x).
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 unh_0: forall dX j, 0 < fst dX -> snd dX <> 0 -> ni_exact xmin xmax dX ->
   (0 <= j <= ni (fst dX))%Z -> unh dX j 0 = ubar xmin usol dX j 0.

Lemma convergence_error_is_discrete_sol: forall dX j n,
  0 < fst dX -> 0 < snd dX -> ni_exact xmin xmax dX ->
 (0 <= j <= ni (fst dX))%Z ->
  scheme xmin xmax c
      (fun dX j => 0)
      (fun dX j => (convergence_error xmin usol unh dX j 1) / (snd dX))
      (fun dX j m => truncation_error xmin xmax c usol u0h u1h fh dX j (S m))
      (convergence_error xmin usol unh) dX j n = 0.

Lemma condinite1j_aux: forall ph qh dX,
  (snd dX <> 0) ->
  (forall j, Lh c ph dX j 1 = Lh c qh dX j 1) ->
  (forall j, ph j 0%nat = qh j 0%nat) ->
  (forall j, ph j 1%nat = qh j 1%nat).

Lemma e1h_LL1h: forall x dX, 0 < fst dX -> snd dX<>0-> ni_exact xmin xmax dX ->
  (0 < jx (x-xmin) (fst dX) < ni (fst dX))%Z ->
  convergence_error xmin usol unh dX (jx (x-xmin) (fst dX)) 1 / (snd dX) =
  LL1h partial_derive_secondvar c usol (Xxt xmin (x,0) dX) dX.

Lemma condinite1j:
  is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3%nat usol ->
  is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4%nat usol ->
  Oupse
   (fun (x : {x : R | Betw xmin xmax x}) dX => convergence_error xmin usol unh dX (jx (projT1 x-xmin) (fst dX)) 1 / (snd dX))
   (fun dX => fst dX ^2 + snd dX^2).

Lemma condinite1h_aux: forall (P:R*R-> Prop) h g,
  (forall dX, P dX -> 0 < fst dX) ->
  (forall dX, P dX -> ni_exact xmin xmax dX) ->
  OuP P (fun (x : {x : R | Betw xmin xmax x}) dX => Rsqr (h dX (jx (projT1 x-xmin) (fst dX)))) g ->
  OuP P (fun (_:unit) dX => finite_squared_norm_dx (fst dX) (h dX)) g.

Lemma condinite1h:
 is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3%nat usol ->
 is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4%nat usol ->
  Oupse
   (fun (_:unit) dX => finite_norm_dx (fst dX)
               (fun j => convergence_error xmin usol unh dX j 1 / (snd dX)))
   (fun dX => fst dX ^2 +snd dX^2).

Lemma energyiniteh:
 is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3%nat usol ->
 is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4%nat usol ->
 Oupse
  (fun (_:unit) dX =>
    sqrt (energy c (convergence_error xmin usol unh dX) dX 0%nat))
  (fun dX => fst dX ^2 +snd dX^2).

Lemma sum_truncation_error:
   is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3 usol ->
   is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4 usol ->
   Oupse
  (fun (t:{t|Under T t}) dX =>
    snd dX * sum_f 1 (kt (projT1 t) (snd dX)-1)
    (fun n => (finite_norm_dx (fst dX)
                   (fun j => truncation_error xmin xmax c usol u0h u1h fh dX j (S n)))))
  (fun dX => (fst dX)^2+ (snd dX)^2).

Lemma energie:
   is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3 usol ->
   is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4 usol ->
 OupsCFLe
  (fun (t:{t|Under T t}) dX =>
    sqrt (energy c (convergence_error xmin usol unh dX) dX
                            (kt (projT1 t) (snd dX) -1)%nat))
  (fun dX => fst dX ^2 +snd dX^2).

Lemma convergence:
  is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3%nat usol ->
  is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4%nat usol ->
 scheme_is_convergent_of_order xmin xmax T c usol unh eps 2%nat 2%nat.

Lemma convergence_xt:
  is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 3%nat usol ->
  is_sufficiently_regular_n xmin xmax partial_derive_firstvar partial_derive_secondvar 4%nat usol ->
  OupsCFLe
  (fun (X: {x : R | Betw xmin xmax x} * {t : R | Under T t}) (dX : R * R)
        => convergence_error xmin usol unh dX (jx (projT1 (fst X)-xmin) (fst dX)) (kt (projT1 (snd X)) (snd dX)))
  (fun dX : R * R => (fst dX ^ 2 + snd dX ^ 2) / sqrt (fst dX)).

End Conv.