| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (648 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (320 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (87 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (170 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
Global Index
A
add_n [definition, in R_n]add2 [definition, in R_two]
add2_fun [definition, in R_two]
aGe0 [lemma, in alpha]
Ah [definition, in one_d_wave_equation]
Ah_is_linear [lemma, in one_d_wave_equation]
Ah_pos [lemma, in one_d_wave_equation]
Ah_cont [lemma, in one_d_wave_equation]
Ah_eq [lemma, in one_d_wave_equation]
Ah_is_symmetrical [lemma, in one_d_wave_equation]
aLe1 [lemma, in alpha]
alpha [definition, in alpha]
alpha [library]
AlphaDefinition [section, in alpha]
AlphaDefinition.a [variable, in alpha]
AlphaDefinition.aGt0 [variable, in alpha]
alphaOK [section, in alpha]
alphaOK.a [variable, in alpha]
alphaOK.aGt0 [variable, in alpha]
alphaOK.eps [variable, in alpha]
alphaSum [section, in alpha]
alphaSum.a [variable, in alpha]
alphaSum.aGt0 [variable, in alpha]
alpha_err_ok_aux4 [lemma, in alpha]
alpha_err_ok [lemma, in alpha]
alpha_zero2 [lemma, in alpha]
alpha_4 [definition, in dirichlet_aux]
alpha_sym [lemma, in alpha]
alpha_rew [lemma, in alpha]
alpha_err_ok_aux3 [lemma, in alpha]
alpha_conv_le1 [lemma, in dirichlet_aux]
alpha_err_ok_aux1 [lemma, in alpha]
alpha_aux [definition, in dirichlet_aux]
alpha_pos [axiom, in alpha]
alpha_err_ok_nat [lemma, in alpha]
alpha_conv_pos [lemma, in dirichlet_aux]
alpha_err_ok_aux5 [lemma, in alpha]
alpha_ak [lemma, in alpha]
alpha_err_ok_aux2 [lemma, in alpha]
alpha_zero1 [lemma, in alpha]
alpha_conv [definition, in dirichlet_aux]
alpha_sum [lemma, in alpha]
alpha_3 [definition, in dirichlet_aux]
analytic_error [definition, in dirichlet_aux]
analytic_error_debutdeligne [lemma, in dirichlet_aux]
analytic_error_implies_error1 [lemma, in dirichlet_aux]
analytic_error_plusi [lemma, in dirichlet_aux]
analytic_error_le [lemma, in dirichlet_aux]
analytic_error_0_0 [lemma, in dirichlet_aux]
analytic_error_0 [lemma, in dirichlet_aux]
analytic_error_implies_error [lemma, in dirichlet_aux]
analytic_error_findeligne [lemma, in dirichlet_aux]
a_err [lemma, in alpha]
a1Ge [lemma, in alpha]
a1Ge0 [lemma, in alpha]
a1Lt1 [lemma, in alpha]
a1_err [lemma, in alpha]
B
Betw [definition, in BigO]BigO [library]
BigOuP [section, in BigO]
BigOuP.A [variable, in BigO]
BigOuP2 [section, in BigO]
blop [abbreviation, in consistency]
C
c [definition, in dirichlet_aux]Calcula [section, in alpha]
Calculaaux [section, in alpha]
Calculaaux.f [variable, in alpha]
Calculaaux.feq [variable, in alpha]
Calculaaux.x [variable, in alpha]
Calculaaux.xGe [variable, in alpha]
CalculaEquatlities [section, in alpha]
Calcula.a [variable, in alpha]
Calcula.aeq [variable, in alpha]
Calcula.a1 [variable, in alpha]
Calcula.a1eq [variable, in alpha]
Calcula.dt [variable, in alpha]
Calcula.dtEPos [variable, in alpha]
Calcula.dtGe [variable, in alpha]
Calcula.dtPos [variable, in alpha]
Calcula.dx [variable, in alpha]
Calcula.dxEPos [variable, in alpha]
Calcula.dxLe [variable, in alpha]
Calcula.dxPos [variable, in alpha]
Calcula.Reldt [variable, in alpha]
Calcula.Reldx [variable, in alpha]
Calcula.t [variable, in alpha]
Calcula.teq [variable, in alpha]
Calcula.v [variable, in alpha]
Calcula.ValGe [variable, in alpha]
Calcula.ValLe [variable, in alpha]
Calcula.vexact [variable, in alpha]
Calcula.vPos [variable, in alpha]
Calcula1 [section, in alpha]
Calcula1.a1 [variable, in alpha]
Calcula1.a1eq [variable, in alpha]
Calcula1.dt [variable, in alpha]
Calcula1.dtGe [variable, in alpha]
Calcula1.dtPos [variable, in alpha]
Calcula1.dx [variable, in alpha]
Calcula1.dxEPos [variable, in alpha]
Calcula1.dxLe [variable, in alpha]
Calcula1.dxPos [variable, in alpha]
Calcula1.Reldt [variable, in alpha]
Calcula1.Reldx [variable, in alpha]
Calcula1.t [variable, in alpha]
Calcula1.teq [variable, in alpha]
Calcula1.v [variable, in alpha]
Calcula1.ValGe [variable, in alpha]
Calcula1.ValLe [variable, in alpha]
Calcula1.vexact [variable, in alpha]
Calcula1.vPos [variable, in alpha]
Cauchy_Schwarz [lemma, in R_n]
CFL [definition, in one_d_wave_equation]
CFL_condition_r [definition, in one_d_wave_equation]
comput1 [library]
condinite1h [lemma, in convergence]
condinite1h_aux [lemma, in convergence]
condinite1j [lemma, in convergence]
condinite1j_aux [lemma, in convergence]
Consistency [section, in consistency]
consistency [lemma, in consistency]
consistency [library]
Consistency.c [variable, in consistency]
Consistency.c_neq_0 [variable, in consistency]
Consistency.f [variable, in consistency]
Consistency.fh [variable, in consistency]
Consistency.f_is_zero_at_beginning [variable, in consistency]
Consistency.partial_derive_secondvar [variable, in consistency]
Consistency.partial_derive_firstvar [variable, in consistency]
Consistency.T [variable, in consistency]
Consistency.T_pos [variable, in consistency]
Consistency.usol [variable, in consistency]
Consistency.usol_is_sol [variable, in consistency]
Consistency.u0 [variable, in consistency]
Consistency.u0h [variable, in consistency]
Consistency.u1 [variable, in consistency]
Consistency.u1h [variable, in consistency]
Consistency.xmax [variable, in consistency]
Consistency.xmin [variable, in consistency]
Consistency.xminLtxmax [variable, in consistency]
construct_alpha [lemma, in dirichlet_aux]
Conv [section, in convergence]
convergence [lemma, in convergence]
convergence [library]
convergence_error [definition, in one_d_wave_equation]
convergence_error_is_discrete_sol [lemma, in convergence]
convergence_xt [lemma, in convergence]
Conv.c [variable, in convergence]
Conv.c_pos [variable, in convergence]
Conv.eps [variable, in convergence]
Conv.eps_lt [variable, in convergence]
Conv.f [variable, in convergence]
Conv.fh [variable, in convergence]
Conv.f_is_zero_at_beginning [variable, in convergence]
Conv.partial_derive_firstvar [variable, in convergence]
Conv.partial_derive_secondvar [variable, in convergence]
Conv.T [variable, in convergence]
Conv.T_pos [variable, in convergence]
Conv.unh [variable, in convergence]
Conv.unh_is_discrete_sol [variable, in convergence]
Conv.usol [variable, in convergence]
Conv.usol_is_sol [variable, in convergence]
Conv.u0 [variable, in convergence]
Conv.u0h [variable, in convergence]
Conv.u1 [variable, in convergence]
Conv.u1h [variable, in convergence]
Conv.xmax [variable, in convergence]
Conv.xmin [variable, in convergence]
Conv.xminLtxmax [variable, in convergence]
C_conv [definition, in dirichlet_aux]
C_conv_pos [lemma, in dirichlet_aux]
C_4 [definition, in dirichlet_aux]
c_pos [lemma, in dirichlet_aux]
C_3 [definition, in dirichlet_aux]
D
defs [section, in R_two]defs.A [variable, in R_two]
defs.B [variable, in R_two]
derivable_eq [lemma, in dirichlet_aux]
derivable_psol_11 [lemma, in dirichlet_aux]
derivable_psol_22 [lemma, in dirichlet_aux]
derivable_psol_2 [lemma, in dirichlet_aux]
derivable_psol_1 [lemma, in dirichlet_aux]
DERIVE [axiom, in dirichlet_aux]
DERIVE_def [axiom, in dirichlet_aux]
derive_psol_2 [lemma, in dirichlet_aux]
derive_psol_1 [lemma, in dirichlet_aux]
derive_psol_11 [lemma, in dirichlet_aux]
DERIVE_eq [lemma, in dirichlet_aux]
derive_psol_22 [lemma, in dirichlet_aux]
Derx [variable, in dirichlet_aux]
Dery [variable, in dirichlet_aux]
Diff [section, in Differential]
differential [definition, in Differential]
Differential [library]
Diff.partial_derive_firstvar [variable, in Differential]
Diff.partial_derive_secondvar [variable, in Differential]
Diff.xmax [variable, in Differential]
Diff.xmin [variable, in Differential]
Diff.xminLtxmax [variable, in Differential]
dirichlet_aux [library]
dirichlet_why [library]
discretization [definition, in one_d_wave_equation]
discr_neg [lemma, in Reals_compl]
divide2_fun [definition, in R_two]
DL_discretization_eps_aux [lemma, in Differential]
DL_discretization_eps_dx [lemma, in Differential]
DL_pol [definition, in Differential]
DL_discretization_eps_dt [lemma, in Differential]
dot_product_n_scal_mult_r [lemma, in R_n]
dot_product_n_eq_suf_l [lemma, in R_n]
dot_product_n_scal_mult_l [lemma, in R_n]
dot_product_n_le_reverse [lemma, in R_n]
dot_product_n_le2 [lemma, in R_n]
dot_product_n_eq_suf_strict_l [lemma, in R_n]
dot_product_n_sym [lemma, in R_n]
dot_product_n_sub_distr_r [lemma, in R_n]
dot_product_n_le [lemma, in R_n]
dot_product_n_shift_indices [lemma, in R_n]
dot_product_n_distr_r [lemma, in R_n]
dot_product_n_zero [lemma, in R_n]
dot_product_n_sub_distr_l [lemma, in R_n]
dot_product_n [definition, in R_n]
dot_product_n_eq_suf_strict_r [lemma, in R_n]
dot_product_n_eq_suf_r [lemma, in R_n]
dot_product_n_distr_l [lemma, in R_n]
doubleP [definition, in dirichlet_aux]
double_xP [definition, in dirichlet_aux]
dtdxLe [lemma, in alpha]
dtGe2 [lemma, in alpha]
E
energie [lemma, in convergence]energy [abbreviation, in convergence]
energy [definition, in one_d_wave_equation]
energy [abbreviation, in stability]
energyiniteh [lemma, in convergence]
energy_pos [lemma, in stability]
energy_majoration_zero [lemma, in stability]
energy_increases [lemma, in stability]
energy_majoration [lemma, in stability]
energy_majoration_aux [lemma, in stability]
epik_step1_FPerrorr [lemma, in comput1]
epik_one_step_FPerrorr [lemma, in comput1]
eps [definition, in dirichlet_aux]
eps_sym1 [lemma, in dirichlet_aux]
eps_sym2 [lemma, in dirichlet_aux]
eps_eps_aux [lemma, in dirichlet_aux]
eps_aux2 [definition, in dirichlet_aux]
eps_0 [lemma, in dirichlet_aux]
eps_aux1 [definition, in dirichlet_aux]
eps_ni [lemma, in dirichlet_aux]
Equiv [section, in Why2Gappa]
equiv_RNDs_aux3 [lemma, in Why2Gappa]
equiv_RNDs_s [lemma, in Why2Gappa]
equiv_RNDs_aux2 [lemma, in Why2Gappa]
equiv_RNDs_aux1 [lemma, in Why2Gappa]
equiv_RNDs [lemma, in Why2Gappa]
equiv_RNDs_aux4 [lemma, in Why2Gappa]
equiv_RNDs_d [lemma, in Why2Gappa]
Equiv.b [variable, in Why2Gappa]
Equiv.p [variable, in Why2Gappa]
Equiv.pGivesBound [variable, in Why2Gappa]
Equiv.precisionNotZero [variable, in Why2Gappa]
Err [definition, in alpha]
Err_ni_aux [lemma, in dirichlet_aux]
Err_0_sym [lemma, in dirichlet_aux]
Err_0_aux [lemma, in dirichlet_aux]
Err_ni_sym [lemma, in dirichlet_aux]
Err_0 [lemma, in dirichlet_aux]
Err_ni [lemma, in dirichlet_aux]
e1h_LL1h [lemma, in convergence]
F
finite_dot_product_dx_eq_strict_r [lemma, in R_n]finite_dot_product_dx_scal_mult_l [lemma, in R_n]
finite_dot_product_dx_zero1 [lemma, in R_n]
finite_dot_product_dx_sub_r [lemma, in R_n]
finite_squared_norm_parall_sub [lemma, in R_n]
finite_squared_norm_dx_pos [lemma, in R_n]
finite_squared_norm_parall [lemma, in R_n]
finite_squared_norm_parall_add [lemma, in R_n]
finite_dot_product_dx_add_l [lemma, in R_n]
finite_dot_product_dx_scal_mult_r [lemma, in R_n]
finite_squared_norm_dx [definition, in R_n]
finite_squared_norm_dx [abbreviation, in consistency]
finite_dot_product_dx_add_r [lemma, in R_n]
finite_norm_dx [definition, in R_n]
finite_dot_product_dx_zero1ou2 [lemma, in R_n]
finite_squared_norm_dx_majoration [lemma, in R_n]
finite_dot_product_le2 [lemma, in R_n]
finite_norm_le [lemma, in R_n]
finite_dot_product_dx_sub_l [lemma, in R_n]
finite_dot_product_dx_sym [lemma, in R_n]
finite_squared_norm_dx_homogen [lemma, in R_n]
finite_dot_product_dx [definition, in R_n]
finite_squared_norm_dx_eq [lemma, in R_n]
finite_norm_dx [abbreviation, in stability]
finite_squared_norm_dx [abbreviation, in stability]
finite_Cauchy_Schwarz_dx [lemma, in R_n]
finite_norm_dx [abbreviation, in convergence]
finite_dot_product_dx [abbreviation, in one_d_wave_equation]
finite_squared_norm_dx_triang [lemma, in R_n]
finite_dot_product_le [lemma, in R_n]
finite_dot_product_dx_shift_indices [lemma, in R_n]
finite_norm_dx [abbreviation, in one_d_wave_equation]
finite_dot_product_dx_eq_strict_l [lemma, in R_n]
finite_norm_le_reverse [lemma, in R_n]
finite_squared_norm_dx [abbreviation, in convergence]
finite_squared_norm_dx_zero [lemma, in R_n]
finite_dot_product_dx_eq_r [lemma, in R_n]
finite_squared_norm_dx [abbreviation, in one_d_wave_equation]
finite_dot_product_dx [abbreviation, in stability]
finite_dot_product_dx_eq_l [lemma, in R_n]
forward_prop_safety_po_80 [lemma, in dirichlet_why]
forward_prop_safety_po_7 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_6 [lemma, in dirichlet_why]
forward_prop_safety_po_18 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_38 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_33 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_14 [lemma, in dirichlet_why]
forward_prop_safety_po_97 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_25 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_18 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_32 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_31 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_8 [lemma, in dirichlet_why]
forward_prop_safety_po_46 [lemma, in dirichlet_why]
forward_prop_safety_po_58 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_11 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_15 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_5 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_7 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_43 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_4 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_44 [lemma, in dirichlet_why]
forward_prop_safety_po_95 [lemma, in dirichlet_why]
forward_prop_safety_po_5 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_3 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_35 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_39 [lemma, in dirichlet_why]
forward_prop_safety_po_6 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_34 [lemma, in dirichlet_why]
forward_prop_safety_po_53 [lemma, in dirichlet_why]
forward_prop_safety_po_87 [lemma, in dirichlet_why]
forward_prop_ensures_default_po_24 [lemma, in dirichlet_why]
f1010normal [lemma, in alpha]
G
Green_formula [lemma, in one_d_wave_equation]I
integer_of_int32 [definition, in dirichlet_aux]Int_part_monotone [lemma, in Reals_compl]
Int_part_pos [lemma, in Reals_compl]
Int_part_IZR [lemma, in Reals_compl]
int32 [definition, in dirichlet_aux]
is_discrete_solution [definition, in one_d_wave_equation]
is_solution_psol [lemma, in dirichlet_aux]
is_sufficiently_regular_n [definition, in Differential]
is_solution [definition, in one_d_wave_equation]
J
jx [definition, in Reals_compl]jx_Betw [lemma, in one_d_wave_equation]
K
kt [definition, in Reals_compl]kt_le [lemma, in Reals_compl]
kt_eq [lemma, in Reals_compl]
L
L [definition, in one_d_wave_equation]Lh [definition, in one_d_wave_equation]
Lh_is_linear [lemma, in one_d_wave_equation]
LL1h [definition, in one_d_wave_equation]
LL1h_is_second_order [lemma, in consistency]
ln_monotone [lemma, in dirichlet_aux]
L0 [definition, in one_d_wave_equation]
L1 [definition, in one_d_wave_equation]
M
max_double_eq [lemma, in Why2Gappa]minorationenergy [lemma, in stability]
minorationenergy2 [lemma, in stability]
multiply2_fun [definition, in R_two]
my_unh [section, in one_d_wave_equation]
my_unh.c [variable, in one_d_wave_equation]
my_proj [definition, in Differential]
my_unh.xmin [variable, in one_d_wave_equation]
my_unh [definition, in one_d_wave_equation]
my_unh.xmax [variable, in one_d_wave_equation]
my_proj [abbreviation, in consistency]
my_unh.u0h [variable, in one_d_wave_equation]
my_unh_correct [lemma, in one_d_wave_equation]
my_unh.u1h [variable, in one_d_wave_equation]
my_unh.fh [variable, in one_d_wave_equation]
N
ni [abbreviation, in one_d_wave_equation]ni [abbreviation, in one_d_wave_equation]
ni [definition, in R_n]
ni [abbreviation, in stability]
ni [abbreviation, in consistency]
ni [abbreviation, in one_d_wave_equation]
ni [abbreviation, in convergence]
ni_exact [definition, in one_d_wave_equation]
ni_Zabs_nat [lemma, in R_n]
ni_pos [lemma, in R_n]
norm_l2_proj2 [lemma, in R_two]
norm_l2_scalar_mult [lemma, in R_two]
norm_l2_proj1 [lemma, in R_two]
norm_dx_conv_err_eq [lemma, in dirichlet_aux]
norm_l2_pos_strict [lemma, in R_two]
norm_l2 [definition, in R_two]
norm_dx_conv_err [definition, in dirichlet_aux]
norm_l2_pos [lemma, in R_two]
O
one_d_wave_equation [library]Ou [abbreviation, in BigO]
OuP [definition, in BigO]
Oup [abbreviation, in BigO]
Oups [abbreviation, in BigO]
OupsCFLe [abbreviation, in one_d_wave_equation]
OupsCFLe [abbreviation, in convergence]
Oupse [abbreviation, in one_d_wave_equation]
Oupse [abbreviation, in consistency]
Oupse [abbreviation, in convergence]
OuP_sum_ortho [lemma, in BigO]
OuP_divide1 [lemma, in BigO]
OuP_every_implies_OuP_here_2 [lemma, in BigO]
OuP_match [lemma, in BigO]
OuP_X_to_appr_Betw [lemma, in consistency]
OuP_divide2 [lemma, in BigO]
OuP_eq_trans_l [lemma, in BigO]
OuP_implies_OuP2 [lemma, in BigO]
OuP_implies_OuP1 [lemma, in BigO]
OuP_multiply2 [lemma, in BigO]
OuP_multiplyAA_z [lemma, in BigO]
OuP_eq_trans_r [lemma, in BigO]
Oup_pointwise_to_squared_norm_dx_truncation_error [lemma, in consistency]
OuP_is_EV_mult [lemma, in BigO]
OuP_multiply1 [lemma, in BigO]
OuP_X_to_appr_fst [lemma, in BigO]
OuP_maj [lemma, in BigO]
OuP_Rabs [lemma, in BigO]
OuP_division [lemma, in BigO]
OuP_snddX_to_dX [lemma, in BigO]
OuP_sum_f [lemma, in BigO]
OuP_inclusion [lemma, in BigO]
OuP_sum_f_minus1_bis [lemma, in BigO]
OuP_X_to_appr_fst_Betw [lemma, in consistency]
OuP_is_EV_mult_z [lemma, in BigO]
OuP_multiplyAA [lemma, in BigO]
OuP_unit [lemma, in BigO]
OuP_every_implies_OuP_here [lemma, in BigO]
OuP_dX_to_eps [lemma, in BigO]
OuP_is_EV_zero [lemma, in BigO]
Oup_pointwise_to_squared_norm_dx [lemma, in consistency]
OuP_case [lemma, in BigO]
OuP_X_to_x [lemma, in BigO]
OuP_implies_OuPMinus [lemma, in BigO]
OuP_dX_to_eps_Betw [lemma, in Differential]
OuP_Rsqr [lemma, in BigO]
OuP_X_to_appr [lemma, in BigO]
OuP_implies_OuP [lemma, in BigO]
OuP_sqrt [lemma, in BigO]
OuP_is_EV_plus [lemma, in BigO]
P
partial_derive_firstvar_n [definition, in Differential]partial_derive_secondvar_n [definition, in Differential]
partial_derive [definition, in Differential]
pointwise_consistency [lemma, in consistency]
powerRZ_1000_eq [lemma, in alpha]
powerRZ_51_eq [lemma, in alpha]
powerRZ_50_eq [lemma, in alpha]
powerRZ_53_eq [lemma, in alpha]
psol [definition, in dirichlet_aux]
psol_Taylor_3 [definition, in dirichlet_aux]
psol_2_def [lemma, in dirichlet_aux]
psol_reg_4 [lemma, in dirichlet_aux]
psol_22_def [lemma, in dirichlet_aux]
psol_suff_regular_3 [lemma, in dirichlet_aux]
psol_22 [definition, in dirichlet_aux]
psol_1 [definition, in dirichlet_aux]
psol_1_def [lemma, in dirichlet_aux]
psol_Taylor_4 [definition, in dirichlet_aux]
psol_suff_regular_4 [lemma, in dirichlet_aux]
psol_11_def [lemma, in dirichlet_aux]
psol_2 [definition, in dirichlet_aux]
psol_11 [definition, in dirichlet_aux]
psol_reg_3 [lemma, in dirichlet_aux]
psol_le [lemma, in dirichlet_aux]
p0 [definition, in dirichlet_aux]
p0h [variable, in dirichlet_aux]
R
Rabs_snd_le_norm_l2 [lemma, in R_two]Rabs_eq [lemma, in Why2Gappa]
Rabs_fst_le_norm_l2 [lemma, in R_two]
Rabs_le_trans [lemma, in alpha]
Reals_compl [library]
Rminus_Int_part_le [lemma, in Reals_compl]
Rmult_eq_compat_r [lemma, in Reals_compl]
Rn [section, in R_n]
Rn.xmax [variable, in R_n]
Rn.xmin [variable, in R_n]
Rn.xminLtxmax [variable, in R_n]
_ + _ (type_scope) [notation, in R_n]
_ - _ (type_scope) [notation, in R_n]
RoudGeOv2 [lemma, in alpha]
RoundErrLe1 [lemma, in alpha]
RoundErrLe2 [lemma, in alpha]
RoundGe1010 [lemma, in alpha]
Rplus_eq_compat [lemma, in alpha]
Rplus_Int_part_ge [lemma, in Reals_compl]
Rplus_eq_compat_r [lemma, in Reals_compl]
Rpower_Rpower [lemma, in dirichlet_aux]
R_two [library]
R_n [library]
S
same_block_shift [lemma, in dirichlet_aux]scalar_multiplyAA_fun [definition, in R_two]
scalar_multiply2 [definition, in R_two]
scalar_multiply_n [definition, in R_n]
scalar_multiplyA_fun [definition, in R_two]
scheme [definition, in one_d_wave_equation]
scheme [abbreviation, in consistency]
scheme_is_convergent_of_order [definition, in one_d_wave_equation]
scheme_eq_1 [lemma, in one_d_wave_equation]
scheme_eq_3 [lemma, in one_d_wave_equation]
scheme_eq_2 [lemma, in one_d_wave_equation]
scheme_is_consistent_of_order [definition, in one_d_wave_equation]
scheme_eq [lemma, in one_d_wave_equation]
semi_finite_dot_product_dx [lemma, in R_n]
separated_matrix_scheme [lemma, in dirichlet_aux]
separated_matrix_eps [lemma, in dirichlet_aux]
separated_matrix_prop [lemma, in dirichlet_aux]
separated_matrix [definition, in dirichlet_aux]
sqr [definition, in dirichlet_aux]
sqrt_pos [lemma, in Reals_compl]
sqr_norm_dx_conv_err_0 [lemma, in dirichlet_aux]
sqr_norm_dx_conv_err_succ [lemma, in dirichlet_aux]
sqr_norm_dx_conv_err [definition, in dirichlet_aux]
squared_norm_n_plus [lemma, in R_n]
squared_norm_n_pos [lemma, in R_n]
squared_norm_n_scal_mult_n [lemma, in R_n]
squared_norm_n [definition, in R_n]
squared_norm_n_majoration [lemma, in R_n]
squared_norm_n_pos_aux [lemma, in R_n]
Stab [section, in stability]
stability [library]
Stab.c [variable, in stability]
Stab.CFL_eps [variable, in stability]
Stab.c_pos [variable, in stability]
Stab.dX [variable, in stability]
Stab.eps [variable, in stability]
Stab.eps_lt [variable, in stability]
Stab.fh [variable, in stability]
Stab.unh [variable, in stability]
Stab.unh_is_discrete_sol [variable, in stability]
Stab.usol [variable, in stability]
Stab.u0h [variable, in stability]
Stab.u1h [variable, in stability]
Stab.xmax [variable, in stability]
Stab.xmin [variable, in stability]
Stab.xminLtxmax [variable, in stability]
subtract_n [definition, in R_n]
subtract2 [definition, in R_two]
subtract2_fun [definition, in R_two]
sum_f_z_Rabs [lemma, in alpha]
sum_f_z_split_aux [lemma, in alpha]
sum_f_z_plus [lemma, in alpha]
sum_f_z_aux [definition, in alpha]
sum_f_z_switch [lemma, in alpha]
sum_f_z_up [lemma, in alpha]
sum_f_z_zero [lemma, in alpha]
sum_f_S [lemma, in Reals_compl]
sum_f_triang [lemma, in Reals_compl]
sum_f_z_up_aux [lemma, in alpha]
Sum_Z_Z [section, in alpha]
sum_f_z_shift1 [lemma, in alpha]
sum_f_z_shift [lemma, in alpha]
sum_f_z_mult [lemma, in alpha]
sum_f_S_Rabs_minus1 [lemma, in Reals_compl]
sum_f_z_cte [lemma, in alpha]
sum_f_Rabs_minus1 [lemma, in Reals_compl]
sum_f_z_le [lemma, in alpha]
sum_f_z_eq [lemma, in alpha]
sum_f_le [lemma, in Reals_compl]
sum_truncation_error [lemma, in convergence]
sum_f_z_1 [lemma, in alpha]
sum_f_z_pos [lemma, in alpha]
sum_f_z [definition, in alpha]
sum_f_z_shift2 [lemma, in alpha]
sum_f_z_split [lemma, in alpha]
sum_f_pos [lemma, in Reals_compl]
sum_f_z_down [lemma, in alpha]
sum_f [definition, in Reals_compl]
T
truncation_error [definition, in one_d_wave_equation]tvGe [lemma, in alpha]
T_max [definition, in dirichlet_aux]
T_max_pos [lemma, in dirichlet_aux]
U
ubar [definition, in one_d_wave_equation]Under [definition, in BigO]
unh_0 [lemma, in convergence]
up_gt_zero [lemma, in Reals_compl]
V
ValGe2 [lemma, in alpha]ValLe2 [lemma, in alpha]
W
Wave [section, in one_d_wave_equation]wave_eq_2 [lemma, in dirichlet_aux]
wave_eq_dirichlet_2 [lemma, in dirichlet_aux]
wave_eq_0 [lemma, in dirichlet_aux]
wave_eq_dirichlet_1 [lemma, in dirichlet_aux]
wave_eq_1 [lemma, in dirichlet_aux]
Wave.c [variable, in one_d_wave_equation]
Wave.eps [variable, in one_d_wave_equation]
Wave.eps_lt [variable, in one_d_wave_equation]
Wave.f [variable, in one_d_wave_equation]
Wave.fh [variable, in one_d_wave_equation]
Wave.partial_derive_firstvar [variable, in one_d_wave_equation]
Wave.partial_derive_secondvar [variable, in one_d_wave_equation]
Wave.T [variable, in one_d_wave_equation]
Wave.T_pos [variable, in one_d_wave_equation]
Wave.unh [variable, in one_d_wave_equation]
Wave.usol [variable, in one_d_wave_equation]
Wave.usol_is_sol [variable, in one_d_wave_equation]
Wave.u0 [variable, in one_d_wave_equation]
Wave.u0h [variable, in one_d_wave_equation]
Wave.u1 [variable, in one_d_wave_equation]
Wave.u1h [variable, in one_d_wave_equation]
Wave.xmax [variable, in one_d_wave_equation]
Wave.xmin [variable, in one_d_wave_equation]
Wave.xminLtxmax [variable, in one_d_wave_equation]
Why2Gappa [library]
X
Xjk [definition, in one_d_wave_equation]Xjk_Betw_j [lemma, in one_d_wave_equation]
Xjk_Betw [lemma, in one_d_wave_equation]
Xxt [definition, in one_d_wave_equation]
Xxtd [abbreviation, in consistency]
Z
Zdichotomy [lemma, in dirichlet_aux]zeroness [section, in one_d_wave_equation]
zeroness_usol_xmin_ni [lemma, in one_d_wave_equation]
zeroness_ubar_1 [lemma, in one_d_wave_equation]
zeroness_ubar_2 [lemma, in one_d_wave_equation]
zeroness_unh_1 [lemma, in one_d_wave_equation]
zeroness_unh_2 [lemma, in one_d_wave_equation]
zeroness.c [variable, in one_d_wave_equation]
zeroness.dX [variable, in one_d_wave_equation]
zeroness.fh [variable, in one_d_wave_equation]
zeroness.unh [variable, in one_d_wave_equation]
zeroness.unh_is_discrete_sol [variable, in one_d_wave_equation]
zeroness.u0h [variable, in one_d_wave_equation]
zeroness.u1h [variable, in one_d_wave_equation]
zeroness.xmax [variable, in one_d_wave_equation]
zeroness.xmin [variable, in one_d_wave_equation]
zeroness.xminLtxmax [variable, in one_d_wave_equation]
zeroness2 [section, in one_d_wave_equation]
zeroness2.c [variable, in one_d_wave_equation]
zeroness2.dX [variable, in one_d_wave_equation]
zeroness2.f [variable, in one_d_wave_equation]
zeroness2.partial_derive_secondvar [variable, in one_d_wave_equation]
zeroness2.partial_derive_firstvar [variable, in one_d_wave_equation]
zeroness2.usol [variable, in one_d_wave_equation]
zeroness2.usol_is_sol [variable, in one_d_wave_equation]
zeroness2.u0 [variable, in one_d_wave_equation]
zeroness2.u1 [variable, in one_d_wave_equation]
zeroness2.xmax [variable, in one_d_wave_equation]
zeroness2.xmin [variable, in one_d_wave_equation]
zeroness2.xminLtxmax [variable, in one_d_wave_equation]
other
_ - _ (type_scope) [notation, in R_two]_ + _ (type_scope) [notation, in R_two]
Lemma Index
A
aGe0 [in alpha]Ah_is_linear [in one_d_wave_equation]
Ah_pos [in one_d_wave_equation]
Ah_cont [in one_d_wave_equation]
Ah_eq [in one_d_wave_equation]
Ah_is_symmetrical [in one_d_wave_equation]
aLe1 [in alpha]
alpha_err_ok_aux4 [in alpha]
alpha_err_ok [in alpha]
alpha_zero2 [in alpha]
alpha_sym [in alpha]
alpha_rew [in alpha]
alpha_err_ok_aux3 [in alpha]
alpha_conv_le1 [in dirichlet_aux]
alpha_err_ok_aux1 [in alpha]
alpha_err_ok_nat [in alpha]
alpha_conv_pos [in dirichlet_aux]
alpha_err_ok_aux5 [in alpha]
alpha_ak [in alpha]
alpha_err_ok_aux2 [in alpha]
alpha_zero1 [in alpha]
alpha_sum [in alpha]
analytic_error_debutdeligne [in dirichlet_aux]
analytic_error_implies_error1 [in dirichlet_aux]
analytic_error_plusi [in dirichlet_aux]
analytic_error_le [in dirichlet_aux]
analytic_error_0_0 [in dirichlet_aux]
analytic_error_0 [in dirichlet_aux]
analytic_error_implies_error [in dirichlet_aux]
analytic_error_findeligne [in dirichlet_aux]
a_err [in alpha]
a1Ge [in alpha]
a1Ge0 [in alpha]
a1Lt1 [in alpha]
a1_err [in alpha]
C
Cauchy_Schwarz [in R_n]condinite1h [in convergence]
condinite1h_aux [in convergence]
condinite1j [in convergence]
condinite1j_aux [in convergence]
consistency [in consistency]
construct_alpha [in dirichlet_aux]
convergence [in convergence]
convergence_error_is_discrete_sol [in convergence]
convergence_xt [in convergence]
C_conv_pos [in dirichlet_aux]
c_pos [in dirichlet_aux]
D
derivable_eq [in dirichlet_aux]derivable_psol_11 [in dirichlet_aux]
derivable_psol_22 [in dirichlet_aux]
derivable_psol_2 [in dirichlet_aux]
derivable_psol_1 [in dirichlet_aux]
derive_psol_2 [in dirichlet_aux]
derive_psol_1 [in dirichlet_aux]
derive_psol_11 [in dirichlet_aux]
DERIVE_eq [in dirichlet_aux]
derive_psol_22 [in dirichlet_aux]
discr_neg [in Reals_compl]
DL_discretization_eps_aux [in Differential]
DL_discretization_eps_dx [in Differential]
DL_discretization_eps_dt [in Differential]
dot_product_n_scal_mult_r [in R_n]
dot_product_n_eq_suf_l [in R_n]
dot_product_n_scal_mult_l [in R_n]
dot_product_n_le_reverse [in R_n]
dot_product_n_le2 [in R_n]
dot_product_n_eq_suf_strict_l [in R_n]
dot_product_n_sym [in R_n]
dot_product_n_sub_distr_r [in R_n]
dot_product_n_le [in R_n]
dot_product_n_shift_indices [in R_n]
dot_product_n_distr_r [in R_n]
dot_product_n_zero [in R_n]
dot_product_n_sub_distr_l [in R_n]
dot_product_n_eq_suf_strict_r [in R_n]
dot_product_n_eq_suf_r [in R_n]
dot_product_n_distr_l [in R_n]
dtdxLe [in alpha]
dtGe2 [in alpha]
E
energie [in convergence]energyiniteh [in convergence]
energy_pos [in stability]
energy_majoration_zero [in stability]
energy_increases [in stability]
energy_majoration [in stability]
energy_majoration_aux [in stability]
epik_step1_FPerrorr [in comput1]
epik_one_step_FPerrorr [in comput1]
eps_sym1 [in dirichlet_aux]
eps_sym2 [in dirichlet_aux]
eps_eps_aux [in dirichlet_aux]
eps_0 [in dirichlet_aux]
eps_ni [in dirichlet_aux]
equiv_RNDs_aux3 [in Why2Gappa]
equiv_RNDs_s [in Why2Gappa]
equiv_RNDs_aux2 [in Why2Gappa]
equiv_RNDs_aux1 [in Why2Gappa]
equiv_RNDs [in Why2Gappa]
equiv_RNDs_aux4 [in Why2Gappa]
equiv_RNDs_d [in Why2Gappa]
Err_ni_aux [in dirichlet_aux]
Err_0_sym [in dirichlet_aux]
Err_0_aux [in dirichlet_aux]
Err_ni_sym [in dirichlet_aux]
Err_0 [in dirichlet_aux]
Err_ni [in dirichlet_aux]
e1h_LL1h [in convergence]
F
finite_dot_product_dx_eq_strict_r [in R_n]finite_dot_product_dx_scal_mult_l [in R_n]
finite_dot_product_dx_zero1 [in R_n]
finite_dot_product_dx_sub_r [in R_n]
finite_squared_norm_parall_sub [in R_n]
finite_squared_norm_dx_pos [in R_n]
finite_squared_norm_parall [in R_n]
finite_squared_norm_parall_add [in R_n]
finite_dot_product_dx_add_l [in R_n]
finite_dot_product_dx_scal_mult_r [in R_n]
finite_dot_product_dx_add_r [in R_n]
finite_dot_product_dx_zero1ou2 [in R_n]
finite_squared_norm_dx_majoration [in R_n]
finite_dot_product_le2 [in R_n]
finite_norm_le [in R_n]
finite_dot_product_dx_sub_l [in R_n]
finite_dot_product_dx_sym [in R_n]
finite_squared_norm_dx_homogen [in R_n]
finite_squared_norm_dx_eq [in R_n]
finite_Cauchy_Schwarz_dx [in R_n]
finite_squared_norm_dx_triang [in R_n]
finite_dot_product_le [in R_n]
finite_dot_product_dx_shift_indices [in R_n]
finite_dot_product_dx_eq_strict_l [in R_n]
finite_norm_le_reverse [in R_n]
finite_squared_norm_dx_zero [in R_n]
finite_dot_product_dx_eq_r [in R_n]
finite_dot_product_dx_eq_l [in R_n]
forward_prop_safety_po_80 [in dirichlet_why]
forward_prop_safety_po_7 [in dirichlet_why]
forward_prop_ensures_default_po_6 [in dirichlet_why]
forward_prop_safety_po_18 [in dirichlet_why]
forward_prop_ensures_default_po_38 [in dirichlet_why]
forward_prop_ensures_default_po_33 [in dirichlet_why]
forward_prop_ensures_default_po_14 [in dirichlet_why]
forward_prop_safety_po_97 [in dirichlet_why]
forward_prop_ensures_default_po_25 [in dirichlet_why]
forward_prop_ensures_default_po_18 [in dirichlet_why]
forward_prop_ensures_default_po_32 [in dirichlet_why]
forward_prop_ensures_default_po_31 [in dirichlet_why]
forward_prop_ensures_default_po_8 [in dirichlet_why]
forward_prop_safety_po_46 [in dirichlet_why]
forward_prop_safety_po_58 [in dirichlet_why]
forward_prop_ensures_default_po_11 [in dirichlet_why]
forward_prop_ensures_default_po_15 [in dirichlet_why]
forward_prop_ensures_default_po_5 [in dirichlet_why]
forward_prop_ensures_default_po_7 [in dirichlet_why]
forward_prop_ensures_default_po_43 [in dirichlet_why]
forward_prop_ensures_default_po_4 [in dirichlet_why]
forward_prop_ensures_default_po_44 [in dirichlet_why]
forward_prop_safety_po_95 [in dirichlet_why]
forward_prop_safety_po_5 [in dirichlet_why]
forward_prop_ensures_default_po_3 [in dirichlet_why]
forward_prop_ensures_default_po_35 [in dirichlet_why]
forward_prop_ensures_default_po_39 [in dirichlet_why]
forward_prop_safety_po_6 [in dirichlet_why]
forward_prop_ensures_default_po_34 [in dirichlet_why]
forward_prop_safety_po_53 [in dirichlet_why]
forward_prop_safety_po_87 [in dirichlet_why]
forward_prop_ensures_default_po_24 [in dirichlet_why]
f1010normal [in alpha]
G
Green_formula [in one_d_wave_equation]I
Int_part_monotone [in Reals_compl]Int_part_pos [in Reals_compl]
Int_part_IZR [in Reals_compl]
is_solution_psol [in dirichlet_aux]
J
jx_Betw [in one_d_wave_equation]K
kt_le [in Reals_compl]kt_eq [in Reals_compl]
L
Lh_is_linear [in one_d_wave_equation]LL1h_is_second_order [in consistency]
ln_monotone [in dirichlet_aux]
M
max_double_eq [in Why2Gappa]minorationenergy [in stability]
minorationenergy2 [in stability]
my_unh_correct [in one_d_wave_equation]
N
ni_Zabs_nat [in R_n]ni_pos [in R_n]
norm_l2_proj2 [in R_two]
norm_l2_scalar_mult [in R_two]
norm_l2_proj1 [in R_two]
norm_dx_conv_err_eq [in dirichlet_aux]
norm_l2_pos_strict [in R_two]
norm_l2_pos [in R_two]
O
OuP_sum_ortho [in BigO]OuP_divide1 [in BigO]
OuP_every_implies_OuP_here_2 [in BigO]
OuP_match [in BigO]
OuP_X_to_appr_Betw [in consistency]
OuP_divide2 [in BigO]
OuP_eq_trans_l [in BigO]
OuP_implies_OuP2 [in BigO]
OuP_implies_OuP1 [in BigO]
OuP_multiply2 [in BigO]
OuP_multiplyAA_z [in BigO]
OuP_eq_trans_r [in BigO]
Oup_pointwise_to_squared_norm_dx_truncation_error [in consistency]
OuP_is_EV_mult [in BigO]
OuP_multiply1 [in BigO]
OuP_X_to_appr_fst [in BigO]
OuP_maj [in BigO]
OuP_Rabs [in BigO]
OuP_division [in BigO]
OuP_snddX_to_dX [in BigO]
OuP_sum_f [in BigO]
OuP_inclusion [in BigO]
OuP_sum_f_minus1_bis [in BigO]
OuP_X_to_appr_fst_Betw [in consistency]
OuP_is_EV_mult_z [in BigO]
OuP_multiplyAA [in BigO]
OuP_unit [in BigO]
OuP_every_implies_OuP_here [in BigO]
OuP_dX_to_eps [in BigO]
OuP_is_EV_zero [in BigO]
Oup_pointwise_to_squared_norm_dx [in consistency]
OuP_case [in BigO]
OuP_X_to_x [in BigO]
OuP_implies_OuPMinus [in BigO]
OuP_dX_to_eps_Betw [in Differential]
OuP_Rsqr [in BigO]
OuP_X_to_appr [in BigO]
OuP_implies_OuP [in BigO]
OuP_sqrt [in BigO]
OuP_is_EV_plus [in BigO]
P
pointwise_consistency [in consistency]powerRZ_1000_eq [in alpha]
powerRZ_51_eq [in alpha]
powerRZ_50_eq [in alpha]
powerRZ_53_eq [in alpha]
psol_2_def [in dirichlet_aux]
psol_reg_4 [in dirichlet_aux]
psol_22_def [in dirichlet_aux]
psol_suff_regular_3 [in dirichlet_aux]
psol_1_def [in dirichlet_aux]
psol_suff_regular_4 [in dirichlet_aux]
psol_11_def [in dirichlet_aux]
psol_reg_3 [in dirichlet_aux]
psol_le [in dirichlet_aux]
R
Rabs_snd_le_norm_l2 [in R_two]Rabs_eq [in Why2Gappa]
Rabs_fst_le_norm_l2 [in R_two]
Rabs_le_trans [in alpha]
Rminus_Int_part_le [in Reals_compl]
Rmult_eq_compat_r [in Reals_compl]
RoudGeOv2 [in alpha]
RoundErrLe1 [in alpha]
RoundErrLe2 [in alpha]
RoundGe1010 [in alpha]
Rplus_eq_compat [in alpha]
Rplus_Int_part_ge [in Reals_compl]
Rplus_eq_compat_r [in Reals_compl]
Rpower_Rpower [in dirichlet_aux]
S
same_block_shift [in dirichlet_aux]scheme_eq_1 [in one_d_wave_equation]
scheme_eq_3 [in one_d_wave_equation]
scheme_eq_2 [in one_d_wave_equation]
scheme_eq [in one_d_wave_equation]
semi_finite_dot_product_dx [in R_n]
separated_matrix_scheme [in dirichlet_aux]
separated_matrix_eps [in dirichlet_aux]
separated_matrix_prop [in dirichlet_aux]
sqrt_pos [in Reals_compl]
sqr_norm_dx_conv_err_0 [in dirichlet_aux]
sqr_norm_dx_conv_err_succ [in dirichlet_aux]
squared_norm_n_plus [in R_n]
squared_norm_n_pos [in R_n]
squared_norm_n_scal_mult_n [in R_n]
squared_norm_n_majoration [in R_n]
squared_norm_n_pos_aux [in R_n]
sum_f_z_Rabs [in alpha]
sum_f_z_split_aux [in alpha]
sum_f_z_plus [in alpha]
sum_f_z_switch [in alpha]
sum_f_z_up [in alpha]
sum_f_z_zero [in alpha]
sum_f_S [in Reals_compl]
sum_f_triang [in Reals_compl]
sum_f_z_up_aux [in alpha]
sum_f_z_shift1 [in alpha]
sum_f_z_shift [in alpha]
sum_f_z_mult [in alpha]
sum_f_S_Rabs_minus1 [in Reals_compl]
sum_f_z_cte [in alpha]
sum_f_Rabs_minus1 [in Reals_compl]
sum_f_z_le [in alpha]
sum_f_z_eq [in alpha]
sum_f_le [in Reals_compl]
sum_truncation_error [in convergence]
sum_f_z_1 [in alpha]
sum_f_z_pos [in alpha]
sum_f_z_shift2 [in alpha]
sum_f_z_split [in alpha]
sum_f_pos [in Reals_compl]
sum_f_z_down [in alpha]
T
tvGe [in alpha]T_max_pos [in dirichlet_aux]
U
unh_0 [in convergence]up_gt_zero [in Reals_compl]
V
ValGe2 [in alpha]ValLe2 [in alpha]
W
wave_eq_2 [in dirichlet_aux]wave_eq_dirichlet_2 [in dirichlet_aux]
wave_eq_0 [in dirichlet_aux]
wave_eq_dirichlet_1 [in dirichlet_aux]
wave_eq_1 [in dirichlet_aux]
X
Xjk_Betw_j [in one_d_wave_equation]Xjk_Betw [in one_d_wave_equation]
Z
Zdichotomy [in dirichlet_aux]zeroness_usol_xmin_ni [in one_d_wave_equation]
zeroness_ubar_1 [in one_d_wave_equation]
zeroness_ubar_2 [in one_d_wave_equation]
zeroness_unh_1 [in one_d_wave_equation]
zeroness_unh_2 [in one_d_wave_equation]
Section Index
A
AlphaDefinition [in alpha]alphaOK [in alpha]
alphaSum [in alpha]
B
BigOuP [in BigO]BigOuP2 [in BigO]
C
Calcula [in alpha]Calculaaux [in alpha]
CalculaEquatlities [in alpha]
Calcula1 [in alpha]
Consistency [in consistency]
Conv [in convergence]
D
defs [in R_two]Diff [in Differential]
E
Equiv [in Why2Gappa]M
my_unh [in one_d_wave_equation]R
Rn [in R_n]S
Stab [in stability]Sum_Z_Z [in alpha]
W
Wave [in one_d_wave_equation]Z
zeroness [in one_d_wave_equation]zeroness2 [in one_d_wave_equation]
Notation Index
R
_ + _ (type_scope) [in R_n]_ - _ (type_scope) [in R_n]
other
_ - _ (type_scope) [in R_two]_ + _ (type_scope) [in R_two]
Abbreviation Index
B
blop [in consistency]E
energy [in convergence]energy [in stability]
F
finite_squared_norm_dx [in consistency]finite_norm_dx [in stability]
finite_squared_norm_dx [in stability]
finite_norm_dx [in convergence]
finite_dot_product_dx [in one_d_wave_equation]
finite_norm_dx [in one_d_wave_equation]
finite_squared_norm_dx [in convergence]
finite_squared_norm_dx [in one_d_wave_equation]
finite_dot_product_dx [in stability]
M
my_proj [in consistency]N
ni [in one_d_wave_equation]ni [in one_d_wave_equation]
ni [in stability]
ni [in consistency]
ni [in one_d_wave_equation]
ni [in convergence]
O
Ou [in BigO]Oup [in BigO]
Oups [in BigO]
OupsCFLe [in one_d_wave_equation]
OupsCFLe [in convergence]
Oupse [in one_d_wave_equation]
Oupse [in consistency]
Oupse [in convergence]
S
scheme [in consistency]X
Xxtd [in consistency]Definition Index
A
add_n [in R_n]add2 [in R_two]
add2_fun [in R_two]
Ah [in one_d_wave_equation]
alpha [in alpha]
alpha_4 [in dirichlet_aux]
alpha_aux [in dirichlet_aux]
alpha_conv [in dirichlet_aux]
alpha_3 [in dirichlet_aux]
analytic_error [in dirichlet_aux]
B
Betw [in BigO]C
c [in dirichlet_aux]CFL [in one_d_wave_equation]
CFL_condition_r [in one_d_wave_equation]
convergence_error [in one_d_wave_equation]
C_conv [in dirichlet_aux]
C_4 [in dirichlet_aux]
C_3 [in dirichlet_aux]
D
differential [in Differential]discretization [in one_d_wave_equation]
divide2_fun [in R_two]
DL_pol [in Differential]
dot_product_n [in R_n]
doubleP [in dirichlet_aux]
double_xP [in dirichlet_aux]
E
energy [in one_d_wave_equation]eps [in dirichlet_aux]
eps_aux2 [in dirichlet_aux]
eps_aux1 [in dirichlet_aux]
Err [in alpha]
F
finite_squared_norm_dx [in R_n]finite_norm_dx [in R_n]
finite_dot_product_dx [in R_n]
I
integer_of_int32 [in dirichlet_aux]int32 [in dirichlet_aux]
is_discrete_solution [in one_d_wave_equation]
is_sufficiently_regular_n [in Differential]
is_solution [in one_d_wave_equation]
J
jx [in Reals_compl]K
kt [in Reals_compl]L
L [in one_d_wave_equation]Lh [in one_d_wave_equation]
LL1h [in one_d_wave_equation]
L0 [in one_d_wave_equation]
L1 [in one_d_wave_equation]
M
multiply2_fun [in R_two]my_proj [in Differential]
my_unh [in one_d_wave_equation]
N
ni [in R_n]ni_exact [in one_d_wave_equation]
norm_l2 [in R_two]
norm_dx_conv_err [in dirichlet_aux]
O
OuP [in BigO]P
partial_derive_firstvar_n [in Differential]partial_derive_secondvar_n [in Differential]
partial_derive [in Differential]
psol [in dirichlet_aux]
psol_Taylor_3 [in dirichlet_aux]
psol_22 [in dirichlet_aux]
psol_1 [in dirichlet_aux]
psol_Taylor_4 [in dirichlet_aux]
psol_2 [in dirichlet_aux]
psol_11 [in dirichlet_aux]
p0 [in dirichlet_aux]
S
scalar_multiplyAA_fun [in R_two]scalar_multiply2 [in R_two]
scalar_multiply_n [in R_n]
scalar_multiplyA_fun [in R_two]
scheme [in one_d_wave_equation]
scheme_is_convergent_of_order [in one_d_wave_equation]
scheme_is_consistent_of_order [in one_d_wave_equation]
separated_matrix [in dirichlet_aux]
sqr [in dirichlet_aux]
sqr_norm_dx_conv_err [in dirichlet_aux]
squared_norm_n [in R_n]
subtract_n [in R_n]
subtract2 [in R_two]
subtract2_fun [in R_two]
sum_f_z_aux [in alpha]
sum_f_z [in alpha]
sum_f [in Reals_compl]
T
truncation_error [in one_d_wave_equation]T_max [in dirichlet_aux]
U
ubar [in one_d_wave_equation]Under [in BigO]
X
Xjk [in one_d_wave_equation]Xxt [in one_d_wave_equation]
Axiom Index
A
alpha_pos [in alpha]D
DERIVE [in dirichlet_aux]DERIVE_def [in dirichlet_aux]
Variable Index
A
AlphaDefinition.a [in alpha]AlphaDefinition.aGt0 [in alpha]
alphaOK.a [in alpha]
alphaOK.aGt0 [in alpha]
alphaOK.eps [in alpha]
alphaSum.a [in alpha]
alphaSum.aGt0 [in alpha]
B
BigOuP.A [in BigO]C
Calculaaux.f [in alpha]Calculaaux.feq [in alpha]
Calculaaux.x [in alpha]
Calculaaux.xGe [in alpha]
Calcula.a [in alpha]
Calcula.aeq [in alpha]
Calcula.a1 [in alpha]
Calcula.a1eq [in alpha]
Calcula.dt [in alpha]
Calcula.dtEPos [in alpha]
Calcula.dtGe [in alpha]
Calcula.dtPos [in alpha]
Calcula.dx [in alpha]
Calcula.dxEPos [in alpha]
Calcula.dxLe [in alpha]
Calcula.dxPos [in alpha]
Calcula.Reldt [in alpha]
Calcula.Reldx [in alpha]
Calcula.t [in alpha]
Calcula.teq [in alpha]
Calcula.v [in alpha]
Calcula.ValGe [in alpha]
Calcula.ValLe [in alpha]
Calcula.vexact [in alpha]
Calcula.vPos [in alpha]
Calcula1.a1 [in alpha]
Calcula1.a1eq [in alpha]
Calcula1.dt [in alpha]
Calcula1.dtGe [in alpha]
Calcula1.dtPos [in alpha]
Calcula1.dx [in alpha]
Calcula1.dxEPos [in alpha]
Calcula1.dxLe [in alpha]
Calcula1.dxPos [in alpha]
Calcula1.Reldt [in alpha]
Calcula1.Reldx [in alpha]
Calcula1.t [in alpha]
Calcula1.teq [in alpha]
Calcula1.v [in alpha]
Calcula1.ValGe [in alpha]
Calcula1.ValLe [in alpha]
Calcula1.vexact [in alpha]
Calcula1.vPos [in alpha]
Consistency.c [in consistency]
Consistency.c_neq_0 [in consistency]
Consistency.f [in consistency]
Consistency.fh [in consistency]
Consistency.f_is_zero_at_beginning [in consistency]
Consistency.partial_derive_secondvar [in consistency]
Consistency.partial_derive_firstvar [in consistency]
Consistency.T [in consistency]
Consistency.T_pos [in consistency]
Consistency.usol [in consistency]
Consistency.usol_is_sol [in consistency]
Consistency.u0 [in consistency]
Consistency.u0h [in consistency]
Consistency.u1 [in consistency]
Consistency.u1h [in consistency]
Consistency.xmax [in consistency]
Consistency.xmin [in consistency]
Consistency.xminLtxmax [in consistency]
Conv.c [in convergence]
Conv.c_pos [in convergence]
Conv.eps [in convergence]
Conv.eps_lt [in convergence]
Conv.f [in convergence]
Conv.fh [in convergence]
Conv.f_is_zero_at_beginning [in convergence]
Conv.partial_derive_firstvar [in convergence]
Conv.partial_derive_secondvar [in convergence]
Conv.T [in convergence]
Conv.T_pos [in convergence]
Conv.unh [in convergence]
Conv.unh_is_discrete_sol [in convergence]
Conv.usol [in convergence]
Conv.usol_is_sol [in convergence]
Conv.u0 [in convergence]
Conv.u0h [in convergence]
Conv.u1 [in convergence]
Conv.u1h [in convergence]
Conv.xmax [in convergence]
Conv.xmin [in convergence]
Conv.xminLtxmax [in convergence]
D
defs.A [in R_two]defs.B [in R_two]
Derx [in dirichlet_aux]
Dery [in dirichlet_aux]
Diff.partial_derive_firstvar [in Differential]
Diff.partial_derive_secondvar [in Differential]
Diff.xmax [in Differential]
Diff.xmin [in Differential]
Diff.xminLtxmax [in Differential]
E
Equiv.b [in Why2Gappa]Equiv.p [in Why2Gappa]
Equiv.pGivesBound [in Why2Gappa]
Equiv.precisionNotZero [in Why2Gappa]
M
my_unh.c [in one_d_wave_equation]my_unh.xmin [in one_d_wave_equation]
my_unh.xmax [in one_d_wave_equation]
my_unh.u0h [in one_d_wave_equation]
my_unh.u1h [in one_d_wave_equation]
my_unh.fh [in one_d_wave_equation]
P
p0h [in dirichlet_aux]R
Rn.xmax [in R_n]Rn.xmin [in R_n]
Rn.xminLtxmax [in R_n]
S
Stab.c [in stability]Stab.CFL_eps [in stability]
Stab.c_pos [in stability]
Stab.dX [in stability]
Stab.eps [in stability]
Stab.eps_lt [in stability]
Stab.fh [in stability]
Stab.unh [in stability]
Stab.unh_is_discrete_sol [in stability]
Stab.usol [in stability]
Stab.u0h [in stability]
Stab.u1h [in stability]
Stab.xmax [in stability]
Stab.xmin [in stability]
Stab.xminLtxmax [in stability]
W
Wave.c [in one_d_wave_equation]Wave.eps [in one_d_wave_equation]
Wave.eps_lt [in one_d_wave_equation]
Wave.f [in one_d_wave_equation]
Wave.fh [in one_d_wave_equation]
Wave.partial_derive_firstvar [in one_d_wave_equation]
Wave.partial_derive_secondvar [in one_d_wave_equation]
Wave.T [in one_d_wave_equation]
Wave.T_pos [in one_d_wave_equation]
Wave.unh [in one_d_wave_equation]
Wave.usol [in one_d_wave_equation]
Wave.usol_is_sol [in one_d_wave_equation]
Wave.u0 [in one_d_wave_equation]
Wave.u0h [in one_d_wave_equation]
Wave.u1 [in one_d_wave_equation]
Wave.u1h [in one_d_wave_equation]
Wave.xmax [in one_d_wave_equation]
Wave.xmin [in one_d_wave_equation]
Wave.xminLtxmax [in one_d_wave_equation]
Z
zeroness.c [in one_d_wave_equation]zeroness.dX [in one_d_wave_equation]
zeroness.fh [in one_d_wave_equation]
zeroness.unh [in one_d_wave_equation]
zeroness.unh_is_discrete_sol [in one_d_wave_equation]
zeroness.u0h [in one_d_wave_equation]
zeroness.u1h [in one_d_wave_equation]
zeroness.xmax [in one_d_wave_equation]
zeroness.xmin [in one_d_wave_equation]
zeroness.xminLtxmax [in one_d_wave_equation]
zeroness2.c [in one_d_wave_equation]
zeroness2.dX [in one_d_wave_equation]
zeroness2.f [in one_d_wave_equation]
zeroness2.partial_derive_secondvar [in one_d_wave_equation]
zeroness2.partial_derive_firstvar [in one_d_wave_equation]
zeroness2.usol [in one_d_wave_equation]
zeroness2.usol_is_sol [in one_d_wave_equation]
zeroness2.u0 [in one_d_wave_equation]
zeroness2.u1 [in one_d_wave_equation]
zeroness2.xmax [in one_d_wave_equation]
zeroness2.xmin [in one_d_wave_equation]
zeroness2.xminLtxmax [in one_d_wave_equation]
Library Index
A
alphaB
BigOC
comput1consistency
convergence
D
Differentialdirichlet_aux
dirichlet_why
O
one_d_wave_equationR
Reals_complR_two
R_n
S
stabilityW
Why2Gappa| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (648 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (320 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (87 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (170 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
This page has been generated by coqdoc