IndisputableMonolith.Gravity.WeakFieldConformalRegge

declarations in this module (40)

• theorem conformal_length_sq_exact L96
• def conformal_remainder L112
• theorem conformal_length_sq_taylor2 L117
• theorem conformal_remainder_zero L129
• def edgeSqFirstOrder L139
• def edgeSqSecondOrder L142
• theorem conformal_length_sq_decomposition L149
• def dirichletForm L169
• def quadraticForm L173
• lemma sum_const_mul_right L177
• lemma inner_sum_const L183
• theorem dirichlet_eq_neg_quadratic L192
• theorem dirichlet_form_eq_neg_quadratic L244
• structure WeakFieldReggeData L279
• def bilinearCoefficient L291
• theorem bilinearCoefficient_symm L295
• def SchlaefliRowSum L311
• def secondOrderReggeAction L327
• def edgeArea L348
• theorem edgeArea_symm L351
• theorem dirichletForm_neg L359
• theorem dirichletForm_edgeArea L378
• theorem weak_field_conformal_reduction L410
• theorem weak_field_conformal_reduction_kappa L483
• theorem secondOrderReggeAction_flat L497
• theorem dirichletForm_flat L506
• def edgeAreaGraph L527
• theorem secondOrder_eq_half_laplacian_action L542
• def laplacianCoefficient L573
• theorem laplacianCoefficient_symm L578
• theorem laplacianCoefficient_row_sum L593
• def laplacianReggeData L615
• theorem bilinearCoefficient_laplacianReggeData L625
• theorem schlaefliRowSum_laplacianReggeData L635
• theorem dirichletForm_diag_irrelevant L643
• theorem dirichletForm_edgeArea_laplacianReggeData L662
• theorem weak_field_conformal_reduction_laplacianData L678
• theorem weak_field_conformal_reduction_laplacianData_kappa L688
• structure WeakFieldConformalReggeCert L698
• theorem weakFieldConformalReggeCert L738