Library consistency

Require Export Fourier.
Require Export one_d_wave_equation.
Open Local Scope nat_scope.
Open Local Scope R_scope.

Section Consistency.
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.

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 c_neq_0: c <> 0.
Hypothesis usol_is_sol: is_solution xmin xmax partial_derive_firstvar partial_derive_secondvar c u0 u1 f usol.

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

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

Notation ni x := (ni xmin xmax x).
Notation my_proj := (fun X => my_proj xmin xmax X).
Notation scheme := (fun c u0h u1h fh uh dX j n => scheme xmin xmax c u0h u1h fh uh dX j n).
Notation finite_squared_norm_dx := (fun dx u => (finite_squared_norm_dx xmin xmax dx u)).

Lemma OuP_X_to_appr_fst_Betw: forall (P:R*R->Prop) h g appr,
   (forall x dX, snd (appr (x, 0) dX) = 0) ->
   (forall x dX, P dX -> xmin <= x <= xmax -> xmin <= fst (appr (x,0) dX) <= xmax) ->
   OuP P (fun (x:{x| Betw xmin xmax x}) dX => h (projT1 x, 0) dX) g ->
   OuP P (fun (X:{x| Betw xmin xmax x}*R) dX => h (appr (projT1 (fst X), 0) dX) dX) g.

Lemma OuP_X_to_appr_Betw: forall (P:R*R->Prop) f g appr,
     (forall X dX, P dX -> xmin <= fst X <= xmax -> xmin <= fst (appr X dX) <= xmax) ->
     OuP P (fun (X:{x| Betw xmin xmax x}*R) dX => f (my_proj X) dX) g ->
     OuP P (fun (X:{x| Betw xmin xmax x}*R) dX => f (appr (my_proj X) dX) dX) g.

Lemma LL1h_is_second_order:
   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 ->
  Oups (fun (x:{x| Betw xmin xmax x}) dX => LL1h partial_derive_secondvar c usol ((projT1 x),0) dX)
           (fun dX => fst dX ^2 + snd dX^2).

Lemma pointwise_consistency:
 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 (X:({x| Betw xmin xmax x})*R) dX =>
                         truncation_error xmin xmax c usol u0h u1h fh dX (jx (projT1 (fst X)-xmin) (fst dX)) (kt (snd X) (snd dX)))
      (fun dX => (fst dX)^2 + (snd dX)^2).
Notation blop := (fun X dX => (S (pred (pred (kt (snd X) (snd dX)))))).
Notation Xxtd := (fun (X : {x : R | Betw xmin xmax x} * R) dX => (Xjk xmin dX (jx (projT1 (fst X)-xmin) (fst dX)) (S (pred (pred (kt (snd X) (snd dX))))))).

Lemma Oup_pointwise_to_squared_norm_dx : forall vh, forall g,
  Oupse
    (fun (X:({x| Betw xmin xmax x})*R) dX => vh dX (jx (projT1 (fst X)-xmin) (fst dX)) (kt (snd X) (snd dX)))
    g ->
  Oupse
    (fun (t : {t|Under T t}) dX =>
      finite_squared_norm_dx (fst dX) (fun j => vh dX j (kt (projT1 t) (snd dX))))
    (fun dX => Rsqr (g dX)).

Lemma Oup_pointwise_to_squared_norm_dx_truncation_error: forall g,
  Oupse
    (fun (X:({x| Betw xmin xmax x})*R) dX =>
      truncation_error xmin xmax c usol u0h u1h fh dX (jx ((projT1 (fst X)-xmin)) (fst dX)) (kt (snd X) (snd dX)))
    g ->
  Oupse
    (fun (t : {t|Under T t}) dX =>
      finite_squared_norm_dx (fst dX)
        (fun j => truncation_error xmin xmax c usol u0h u1h fh dX j (kt (projT1 t) (snd dX))))
    (fun dX => Rsqr (g dX)).

Theorem consistency:
  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_consistent_of_order xmin xmax T c usol u0h u1h fh 2%nat 2%nat.

End Consistency.