IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly

declarations in this module (134)

• def heronSq L69
• def hingeArea L72
• def areaGradA L74
• def areaGradB L77
• def areaGradC L80
• lemma hasDerivAt_quad_sub_sq L83
• theorem hasDerivAt_heronSq_a L91
• theorem hasDerivAt_heronSq_b L105
• theorem hasDerivAt_heronSq_c L119
• lemma hasDerivAt_sqrt_heron_coord L133
• theorem hasDerivAt_hingeArea_a L142
• theorem hasDerivAt_hingeArea_b L152
• theorem hasDerivAt_hingeArea_c L161
• theorem heronSq_t11 L172
• theorem heronSq_t12 L173
• theorem heronSq_t13 L174
• theorem heronSq_t22 L175
• theorem hingeArea_t11 L177
• theorem hingeArea_t12 L182
• theorem hingeArea_t13 L189
• theorem hingeArea_t22 L196
• theorem areaGradA_t11 L199
• theorem areaGradB_t11 L201
• theorem areaGradC_t11 L203
• theorem areaGradA_t12 L206
• theorem areaGradB_t12 L213
• theorem areaGradC_t12 L220
• theorem areaGradA_t13 L223
• theorem areaGradB_t13 L230
• theorem areaGradC_t13 L237
• theorem areaGradA_t22 L240
• theorem areaGradB_t22 L242
• theorem areaGradC_t22 L244
• theorem hasDerivAt_area_t11_a L247
• theorem hasDerivAt_area_t11_b L251
• theorem hasDerivAt_area_t11_c L255
• theorem hasDerivAt_area_t12_a L260
• theorem hasDerivAt_area_t12_b L264
• theorem hasDerivAt_area_t12_c L268
• theorem hasDerivAt_area_t13_a L273
• theorem hasDerivAt_area_t13_b L277
• theorem hasDerivAt_area_t13_c L281
• theorem hasDerivAt_area_t22_a L286
• theorem hasDerivAt_area_t22_b L290
• theorem hasDerivAt_area_t22_c L294
• def complementMask L301
• theorem complement_preserves_edge_mask L303
• def kernel21 L315
• def kernel31 L319
• theorem kernel21_eq_kernel12 L322
• theorem kernel31_eq_kernel13 L325
• theorem complement_swaps_type_reexport L328
• def areaCov11 L336
• def areaCov12 L342
• def areaCov21 L348
• def areaCov13 L354
• def areaCov31 L360
• def areaCov22 L366
• theorem areaCov11_eq_grads L372
• theorem areaCov12_eq_grads L378
• theorem areaCov22_eq_grads L384
• def orbitDeficitKernel L392
• def orbitAreaCov L400
• def orbitCellCount L408
• theorem orbitCellCount_eq_classification L416
• def coeffDot L421
• def classDot L424
• def orbitZeroMomQuadratic L427
• def orbitZeroMomBilinear L431
• def trueWeightZeroMomQuadratic L436
• def trueWeightZeroMomBilinear L439
• theorem classDot_add L442
• theorem classDot_smul L447
• theorem orbitZeroMomQuadratic_eq_bilinear L454
• theorem trueWeightZeroMomQuadratic_eq_bilinear L458
• theorem trueWeightZeroMomBilinear_symm L463
• theorem trueWeightZeroMomBilinear_add_left L468
• theorem trueWeightZeroMomBilinear_smul_left L476
• theorem trueWeightZeroMomQuadratic_add L483
• def axisTTPlusCoeffZ L506

… and 54 more