Library dirichlet_aux
Require Export comput1.
Require Export convergence.
Require Export jessie_why.
Open Local Scope Z_scope.
Local Coercion FtoRradix: Float.float >-> R.
DERIVE function is defined as a total function, but its only property
is its correctness when the input is derivable.
Parameter DERIVE: (R->R) -> (R->R).
Axiom DERIVE_def: forall f (H:derivable f), DERIVE f = derive f H.
Let Derx:= fun f (X:R*R) => DERIVE (fun z => f (z,(snd X))) (fst X).
Let Dery:= fun f (X:R*R) => DERIVE (fun z => f ((fst X),z)) (snd X).
Lemma derivable_eq: forall f1 f2, derivable f1 -> (forall x, f1 x = f2 x)
-> derivable f2.
Lemma DERIVE_eq: forall f1 f2 z, derivable f1 -> (forall x, f1 x = f2 x)
-> DERIVE f1 z = DERIVE f2 z.
First Why definitions
Definition doubleP: Set.
Admitted.
Definition double_xP: Set.
Admitted.
Definition int32: Set.
Admitted.
Definition C_3 : R.
Admitted.
Definition C_4 : R.
Admitted.
Definition T_max : R.
Admitted.
Lemma T_max_pos : (Rlt (0)%R T_max).
Admitted.
Definition alpha_3 : R.
Admitted.
Definition alpha_4 : R.
Admitted.
Definition c : R.
Admitted.
Lemma c_pos : (Rlt (0)%R c).
Admitted.
Definition integer_of_int32 : int32 -> Z.
Admitted.
Definition p0 : R -> R.
Admitted.
Definition psol : R -> R -> R.
Admitted.
Definition psol_1 : R -> R -> R.
Admitted.
Definition psol_11 : R -> R -> R.
Admitted.
Lemma psol_11_def :
(forall (x_4:R),
(forall (t_3:R),
(forall (eps_0:R),
(exists C_0:R, (Rlt (0)%R C_0) /\
(forall (dx_0:R),
((Rlt (Rabs dx_0) C_0) ->
(Rlt
(Rabs
(Rminus
(Rdiv (Rminus (psol_1 (Rplus x_4 dx_0) t_3) (psol_1 x_4 t_3)) dx_0) (
psol_11 x_4 t_3)))
eps_0))))))).
Admitted.
Lemma psol_1_def :
(forall (x_2_0:R),
(forall (t_1:R),
(forall (eps:R),
(exists C:R, (Rlt (0)%R C) /\
(forall (dx:R),
((Rlt (Rabs dx) C) ->
(Rlt
(Rabs
(Rminus
(Rdiv (Rminus (psol (Rplus x_2_0 dx) t_1) (psol x_2_0 t_1)) dx) (
psol_1 x_2_0 t_1)))
eps))))))).
Admitted.
Definition psol_2 : R -> R -> R.
Admitted.
Definition psol_22 : R -> R -> R.
Admitted.
Lemma psol_22_def :
(forall (x_8:R),
(forall (t_7:R),
(forall (eps_2:R),
(exists C_2:R, (Rlt (0)%R C_2) /\
(forall (dt_0_0:R),
((Rlt (Rabs dt_0_0) C_2) ->
(Rlt
(Rabs
(Rminus
(Rdiv
(Rminus (psol_2 x_8 (Rplus t_7 dt_0_0)) (psol_2 x_8 t_7)) dt_0_0) (
psol_22 x_8 t_7)))
eps_2))))))).
Admitted.
Lemma psol_2_def :
(forall (x_6:R),
(forall (t_5:R),
(forall (eps_1:R),
(exists C_1:R, (Rlt (0)%R C_1) /\
(forall (dt_0:R),
((Rlt (Rabs dt_0) C_1) ->
(Rlt
(Rabs
(Rminus
(Rdiv (Rminus (psol x_6 (Rplus t_5 dt_0)) (psol x_6 t_5)) dt_0) (
psol_2 x_6 t_5)))
eps_1))))))).
Admitted.
Lemma psol_le :
(forall (x_16:R),
(forall (t_15:R),
((Rle (0)%R x_16) /\ (Rle x_16 (1)%R) ->
((Rle (0)%R t_15) -> (Rle (Rabs (psol x_16 t_15)) (1)%R))))).
Admitted.
Definition psol_Taylor_3 : R -> R -> R -> R -> R.
Defined.
Definition psol_Taylor_4 : R -> R -> R -> R -> R.
Defined.
Lemma psol_suff_regular_3 :
(Rlt (0)%R alpha_3) /\ (Rlt (0)%R C_3) /\
(forall (x_14:R),
(forall (t_13:R),
(forall (dx_3:R),
(forall (dt_3:R),
((Rle (0)%R x_14) /\ (Rle x_14 (1)%R) ->
((Rle (sqrt (Rplus (Rmult dx_3 dx_3) (Rmult dt_3 dt_3))) alpha_3) ->
(Rle
(Rabs
(Rminus
(psol (Rplus x_14 dx_3) (Rplus t_13 dt_3)) (psol_Taylor_3
x_14 t_13 dx_3 dt_3)))
(Rmult
C_3 (Rabs
(Rpower (sqrt (Rplus (Rmult dx_3 dx_3) (Rmult dt_3 dt_3)))
(3)%R)))))))))).
Admitted.
Lemma psol_suff_regular_4 :
(Rlt (0)%R alpha_4) /\ (Rlt (0)%R C_4) /\
(forall (x_15:R),
(forall (t_14:R),
(forall (dx_4:R),
(forall (dt_4:R),
((Rle (0)%R x_15) /\ (Rle x_15 (1)%R) ->
((Rle (sqrt (Rplus (Rmult dx_4 dx_4) (Rmult dt_4 dt_4))) alpha_4) ->
(Rle
(Rabs
(Rminus
(psol (Rplus x_15 dx_4) (Rplus t_14 dt_4)) (psol_Taylor_4
x_15 t_14 dx_4 dt_4)))
(Rmult
C_4 (Rabs
(Rpower (sqrt (Rplus (Rmult dx_4 dx_4) (Rmult dt_4 dt_4)))
(4)%R)))))))))).
Admitted.
Definition separated_matrix (p_1:(pointer double_xP)) (leni:Z) (double_xP_double_xM_p_1_2_at_L:(memory double_xP (pointer doubleP)))
:= (forall (i_1:Z),
(forall (j:Z),
(0 <= i_1 /\ i_1 < leni ->
(0 <= j /\ j < leni ->
(i_1 <> j ->
~(same_block
(select double_xP_double_xM_p_1_2_at_L (shift p_1 i_1)) (
select double_xP_double_xM_p_1_2_at_L (shift p_1 j)))))))).
Definition sqr (x_17:R) := (Rmult x_17 x_17).
Lemma wave_eq_0 :
(forall (x_9:R),
((Rle (0)%R x_9) /\ (Rle x_9 (1)%R) -> (eq (psol x_9 (0)%R) (p0 x_9)))).
Admitted.
Lemma wave_eq_1 :
(forall (x_10:R),
((Rle (0)%R x_10) /\ (Rle x_10 (1)%R) -> (eq (psol_2 x_10 (0)%R) (0)%R))).
Admitted.
Lemma wave_eq_2 :
(forall (x_11:R),
(forall (t_8:R),
((Rle (0)%R x_11) /\ (Rle x_11 (1)%R) ->
(eq (Rminus (psol_22 x_11 t_8) (Rmult (Rmult c c) (psol_11 x_11 t_8))) (0)%R)))).
Admitted.
Lemma wave_eq_dirichlet_1 :
(forall (t_9:R), (eq (psol (0)%R t_9) (0)%R)).
Admitted.
Lemma wave_eq_dirichlet_2 :
(forall (t_10:R), (eq (psol (1)%R t_10) (0)%R)).
Admitted.
Definition of the average of the convergence error
Definition sqr_norm_dx_conv_err :
(pointer double_xP) -> R -> R -> Z -> Z -> Z
-> (memory double_xP (pointer doubleP)) -> (memory doubleP double) -> R.
Defined.
Definition norm_dx_conv_err (p_5:(pointer double_xP)) (dt_10:R) (ni_4:Z) (k_4:Z) (double_xP_double_xM_p_5_4_at_L:(memory double_xP (pointer doubleP))) (double_P_double_M_double_xM_22_at_L:(memory doubleP double))
:= (sqrt
(sqr_norm_dx_conv_err
p_5 (Rdiv (1)%R (IZR ni_4)) dt_10 ni_4 ni_4 k_4 double_xP_double_xM_p_5_4_at_L double_P_double_M_double_xM_22_at_L)).
Lemma norm_dx_conv_err_eq: forall p dt ni k mem1 mem2, 0 <= k -> ni <> 0 ->
norm_dx_conv_err p dt ni k mem1 mem2 =
finite_norm_dx 0 1 (/ni)
(fun z => convergence_error 0 (fun X => psol (fst X) (snd X))
(fun _ j k => double_exact (select mem2 (shift (select mem1 (shift p j)) k)))
(/ni,dt) z (Zabs_nat k)).
Lemma sqr_norm_dx_conv_err_0 :
(forall (double_xP_double_xM_p_3_14_at_L:(memory double_xP (pointer doubleP))),
(forall (double_P_double_M_double_xM_28_at_L:(memory doubleP double)),
(forall (p_3:(pointer double_xP)),
(forall (dx_6:R),
(forall (dt_8:R),
(forall (ni_2:Z),
(forall (k_2:Z),
(eq (sqr_norm_dx_conv_err
p_3 dx_6 dt_8 ni_2 0 k_2 double_xP_double_xM_p_3_14_at_L double_P_double_M_double_xM_28_at_L) (0)%R)))))))).
Lemma sqr_norm_dx_conv_err_succ :
(forall (double_xP_double_xM_p_4_15_at_L:(memory double_xP (pointer doubleP))),
(forall (double_P_double_M_double_xM_16_at_L:(memory doubleP double)),
(forall (p_4:(pointer double_xP)),
(forall (dx_7:R),
(forall (dt_9:R),
(forall (ni_3:Z),
(forall (k_3:Z),
(forall (i_3:Z),
(0 <= i_3 ->
(eq (sqr_norm_dx_conv_err
p_4 dx_7 dt_9 ni_3 (i_3 + 1) k_3 double_xP_double_xM_p_4_15_at_L double_P_double_M_double_xM_16_at_L) (
Rplus
(sqr_norm_dx_conv_err
p_4 dx_7 dt_9 ni_3 i_3 k_3 double_xP_double_xM_p_4_15_at_L double_P_double_M_double_xM_16_at_L) (
Rmult
dx_7 (sqr
(Rminus
(psol
(Rdiv (Rmult (1)%R (IZR i_3)) (IZR ni_3)) (Rmult
(IZR k_3) dt_9)) (
double_exact
(select
double_P_double_M_double_xM_16_at_L (shift
(select
double_xP_double_xM_p_4_15_at_L (
shift p_4 i_3)) k_3))))))))))))))))).
End of first Why definitions
Derive
Lemma derivable_psol_1:
forall x, derivable (fun z => psol z x).
Lemma derive_psol_1:
forall x y, derive (fun z => psol z y) (derivable_psol_1 y) x = psol_1 x y.
Lemma derivable_psol_2:
forall x, derivable (fun z => psol x z).
Lemma derive_psol_2:
forall x y, derive (fun z => psol x z) (derivable_psol_2 x) y = psol_2 x y.
Lemma derivable_psol_11:
forall x, derivable (fun z => psol_1 z x).
Lemma derive_psol_11:
forall x y, derive (fun z => psol_1 z y) (derivable_psol_11 y) x = psol_11 x y.
Lemma derivable_psol_22:
forall x, derivable (fun z => psol_2 x z).
Lemma derive_psol_22:
forall x y, derive (fun z => psol_2 x z) (derivable_psol_22 x) y = psol_22 x y.
Lemma is_solution_psol: is_solution 0 1 Derx Dery c p0 (fun _ : R => Z0) (fun _ : R * R => Z0)
(fun X : R * R => psol (fst X) (snd X)).
Lemma psol_reg_3: is_sufficiently_regular_n 0 1 Derx Dery 3
(fun X : R * R => psol (fst X) (snd X)).
Lemma psol_reg_4: is_sufficiently_regular_n 0 1 Derx Dery 4
(fun X : R * R => psol (fst X) (snd X)).
Let p0h := (fun dX j => p0 (fst (Xjk 0 dX j 0))).
Other Why definitions: C_conv and alpha_conv
Definition C_conv : R.
Defined.
Lemma C_conv_pos: (0 < C_conv)%R.
Definition alpha_aux : R.
Defined.
Lemma ln_monotone: forall x y : R, (0 < x)%R -> (x <= y)%R -> (ln x <= ln y)%R.
Lemma Rpower_Rpower: forall x y z, Rpower (Rpower x y) z = Rpower x (y*z).
Lemma construct_alpha: forall M, (0 < M)%R -> { alp:R |
forall dx dt, (0 < dx)%R -> (0 <= dt)%R -> (sqrt(dx*dx+dt*dt) <= alp)%R ->
(dt / dx * c <= 1)%R ->
((dx*dx+dt*dt) / sqrt dx <= M)%R }.
Definition alpha_conv : R.
Defined.
Lemma alpha_conv_le1: (alpha_conv <= 1)%R.
Lemma alpha_conv_pos :
(Rlt (0)%R alpha_conv).
analytic_error
Lemma Zdichotomy:
forall n m : Z, {n <= m} + {m < n}.
Definition eps_aux1:
(pointer double_xP) -> Z -> double
-> (memory double_xP (pointer doubleP))
-> (memory doubleP double) -> Z -> Z -> R.
Defined.
Definition eps_aux2 :
(pointer double_xP) -> Z -> double
-> (memory double_xP (pointer doubleP))
-> (memory doubleP double) -> Z -> Z -> R.
Defined.
Definition eps :
(pointer double_xP) -> Z -> double
-> (memory double_xP (pointer doubleP))
-> (memory doubleP double) -> Z -> Z -> R.
Defined.
Lemma same_block_shift:
forall (A1 : Set) (p q : pointer A1) (l:Z),
p = shift q l -> same_block p q.
Lemma separated_matrix_prop:
forall p mem1 mem2 ni i1 i2 k1 k2 (d:double),
separated_matrix p ni mem1 ->
(0 <= i1 < ni) -> (0 <= i2 < ni) ->
(i1 <> i2)%Z \/ (k1<>k2)%Z ->
(select (store mem2 (shift (select mem1 (shift p i2)) k2) d) (shift (select mem1 (shift p i1)) k1))
= select mem2 (shift (select mem1 (shift p i1)) k1).
Definition analytic_error :
(pointer double_xP) -> Z -> Z -> Z -> double -> double
-> (memory double_xP (pointer doubleP))
-> (memory doubleP double) -> Prop.
Defined.
Lemma eps_eps_aux: forall p ni i k a mem1 mem2,
0 < ni ->
0 <= i <= ni ->
eps p ni a mem1 mem2 i k = eps_aux1 p ni a mem1 mem2 i k.
Lemma eps_0: forall p ni k a mem1 mem2,
0 < ni ->
eps p ni a mem1 mem2 0 k= 0.
Lemma eps_ni: forall p ni k a mem1 mem2,
0 < ni ->
eps p ni a mem1 mem2 ni k= 0.
Lemma separated_matrix_eps:
forall p mem1 mem2 ni a d i1 i2 k1 k2,
separated_matrix p (ni+1) mem1 ->
(0 <= i2 < ni+1) ->
(0 <= k1) -> (0 <= k2) ->
(k1< k2 \/ (k1=k2 /\ 0 <= i1 < i2)) ->
eps p ni a mem1
((store mem2 (shift (select mem1 (shift p i2)) k2) d))
i1 k1
= eps p ni a mem1 mem2 i1 k1.
Lemma separated_matrix_scheme:
forall p mem1 mem2 ni p0h u1h fh dX i1 k1 i2 k2 d,
separated_matrix p (ni+1) mem1 ->
(fst dX = / (IZR ni)) ->
(0 <= i1 <= ni) ->
(0 <= i2 <= ni) ->
(0 <= k1) -> (0 <= k2) ->
(k1< k2 \/ (k1=k2 /\ i1 < i2)) ->
scheme 0 1 c p0h u1h fh (fun _ i j => double_exact
(select (store mem2 (shift (select mem1 (shift p i2)) k2) d)
(shift (select mem1 (shift p i)) j))) dX i1 (Zabs_nat k1) =
scheme 0 1 c p0h u1h fh (fun _ i j => double_exact
(select mem2 (shift (select mem1 (shift p i)) j))) dX i1 (Zabs_nat k1).
Lemma eps_sym1: forall p ni i k a mem1 mem2,
(0 < ni) ->
(eps p ni a mem1 mem2 (-i) k = - eps p ni a mem1 mem2 i k)%R.
Lemma eps_sym2: forall p ni i k a mem1 mem2,
(0 < ni) ->
(eps p ni a mem1 mem2 (ni-i) k = - eps p ni a mem1 mem2 (ni+i) k)%R.
Lemma Err_0_sym: forall p ni i k a mem1 mem2,
(0 <= k) -> (0 < ni) ->
(Err (double_exact a) (eps p ni a mem1 mem2) i k =
-Err (double_exact a) (eps p ni a mem1 mem2) (-i) k)%R.
Lemma Err_ni_sym: forall p ni i k a mem1 mem2,
(0 <= k) -> (0 < ni) ->
(Err (double_exact a) (eps p ni a mem1 mem2) (ni-i) k =
-Err (double_exact a) (eps p ni a mem1 mem2) (ni+i) k)%R.
Lemma Err_0_aux: forall p ni (k:nat) a mem1 mem2,
(0 < ni) -> (0 < double_exact a)%R ->
(Err (double_exact a) (eps p ni a mem1 mem2) 0 k = 0)%R.
Lemma Err_0: forall p ni k a mem1 mem2,
(0 < ni) -> (0 < double_exact a)%R -> (0 <= k) ->
(Err (double_exact a) (eps p ni a mem1 mem2) 0 k = 0)%R.
Lemma Err_ni_aux: forall p ni (k:nat) a mem1 mem2,
(0 < ni) -> (0 < double_exact a)%R ->
(Err (double_exact a) (eps p ni a mem1 mem2) ni k = 0)%R.
Lemma Err_ni: forall p ni k a mem1 mem2,
(0 < ni) -> (0 < double_exact a)%R -> (0 <= k) ->
(Err (double_exact a) (eps p ni a mem1 mem2) ni k = 0)%R.
Lemma analytic_error_implies_error: forall p ni i k a dt mem1 mem2,
(analytic_error p ni i k a dt mem1 mem2) ->
(0 <= i <= ni)%Z -> (0 <= k)%Z ->
(double_round_error (select mem2 (shift (select mem1 (shift p i)) k))
<= 78*powerRZ 2 (-52)*((k+1)*(k+2)/2))%R.
Lemma analytic_error_implies_error1: forall p ni i1 k1 i k a dt mem1 mem2,
(analytic_error p ni i1 k1 a dt mem1 mem2) ->
(0 <= i <= ni)%Z -> (0 <= k)%Z ->
(0 <= i1 <= ni)%Z -> (0 <= k1)%Z ->
(k < k1 \/ (k=k1 /\ i <= i1)) ->
(double_round_error (select mem2 (shift (select mem1 (shift p i)) k))
<= 78*powerRZ 2 (-52)*((k+1)*(k+2)/2))%R.
Lemma analytic_error_0_0: forall p ni a dt mem1 mem2 mem3 d,
(0 < ni) ->
(0 < double_exact a)%R ->
(mem3=store mem2 (shift (select mem1 (shift p 0)) 0) d) ->
double_value d = 0 ->
double_exact d = 0 ->
(analytic_error p ni 0 0 a dt mem1 mem3).
Lemma analytic_error_0: forall p ni a dt i mem1 mem2 mem3 d,
separated_matrix p (ni+1) mem1 ->
(0 < i < ni)%Z ->
(analytic_error p ni (i-1) 0 a dt mem1 mem2) ->
(mem3=store mem2 (shift (select mem1 (shift p i)) 0) d) ->
(double_round_error d <= 14 * powerRZ radix (-52))%R ->
double_exact d = p0 (IZR i/ni)%R ->
(analytic_error p ni i 0 a dt mem1 mem3).
Lemma analytic_error_plusi : forall p ni i k a dt mem1 mem2 mem3 d r,
separated_matrix p (ni+1) mem1 ->
(0 <= i < ni)%Z -> (0 < k)%Z ->
(analytic_error p ni i k a dt mem1 mem2) ->
(mem3=store mem2 (shift (select mem1 (shift p (i+1))) k) d) ->
(r = eps p ni a mem1 mem3 (i+1)%Z k) ->
(Rabs r <= 78*powerRZ 2 (-52))%R ->
(double_exact d - double_value d = r+
(sum_f_z
(fun l => sum_f_z
(fun j => (alpha (double_exact a) j (Zabs_nat l))
* (eps p ni a mem1 mem2 (i+1+j)%Z (k-l)%Z))
(-l) l)
1 k))%R ->
scheme 0 1 c p0h (fun (_ : R * R) (_ : Z) => Z0)
(fun (_ : R * R) (_ : Z) (_ : nat) => Z0)
(fun (_ : R * R) (l1 : Z) (l2 : nat) =>
double_exact (select mem3 (shift (select mem1 (shift p l1)) l2)))
(/(IZR ni), double_exact dt) (i+1) (Zabs_nat k) = Z0
->
(analytic_error p ni (i+1) k a dt mem1 mem3).
Lemma analytic_error_debutdeligne : forall p ni k a dt mem1 mem2 mem3 d,
separated_matrix p (ni+1) mem1 -> (0 < ni) ->
(0 <= k)%Z -> (0 < double_exact a)%R ->
(analytic_error p ni ni k a dt mem1 mem2) ->
(mem3=store mem2 (shift (select mem1 (shift p 0)) (k+1)) d) ->
double_value d = 0 ->
double_exact d = 0 ->
(analytic_error p ni 0 (k+1) a dt mem1 mem3).
Lemma analytic_error_findeligne : forall p ni k a dt mem1 mem2 mem3 d,
separated_matrix p (ni+1) mem1 -> (1 <= ni) ->
(0 <= k)%Z -> (0 < double_exact a)%R ->
(analytic_error p ni (ni-1) k a dt mem1 mem2) ->
(mem3=store mem2 (shift (select mem1 (shift p ni)) k) d) ->
double_value d = 0 ->
double_exact d = 0 ->
(analytic_error p ni ni k a dt mem1 mem3).
Lemma analytic_error_le :
(forall (double_xP_double_xM_p_0_10_at_L:(memory double_xP (pointer doubleP))),
(forall (double_P_double_M_double_xM_11_at_L:(memory doubleP double)),
(forall (p_0:(pointer double_xP)),
(forall (ni_0_0:Z),
(forall (i_0:Z),
(forall (nk_0:Z),
(forall (k_0:Z),
(forall (a_0:double),
(forall (dt_6:double),
(0 < ni_0_0 ->
(0 <= i_0 /\ i_0 <= ni_0_0 ->
(0 <= k_0 ->
((Rlt (0)%R (double_exact dt_6)) ->
((analytic_error
p_0 ni_0_0 i_0 k_0 a_0 dt_6 double_xP_double_xM_p_0_10_at_L double_P_double_M_double_xM_11_at_L) ->
((Rlt
(sqrt
(Rplus
(Rdiv (1)%R (IZR (ni_0_0 * ni_0_0))) (Rmult
(double_exact dt_6) (
double_exact dt_6))))
alpha_conv) ->
(k_0 <= nk_0 ->
(nk_0 <= 7598581 ->
((Rle (Rmult (IZR nk_0) (double_exact dt_6)) T_max) ->
((Rle (Rmult (Rmult (double_exact dt_6) (IZR ni_0_0)) c)
(Rminus (1)%R (1 / 1125899906842624)%R)) ->
(forall (i1:Z),
(forall (k1:Z),
(0 <= i1 /\ i1 <= ni_0_0 ->
(0 <= k1 /\ k1 < k_0 ->
(Rle
(Rabs
(double_value
(select
double_P_double_M_double_xM_11_at_L (shift
(select
double_xP_double_xM_p_0_10_at_L (
shift
p_0 i1)) k1))))
(2)%R)))))))))))))))))))))))).