IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel

declarations in this module (87)

• abbrev SqEdges4 L67
• def seedFlatSqEdges L71
• lemma seedFlat_0 L75
• lemma seedFlat_1 L76
• lemma seedFlat_2 L77
• lemma seedFlat_3 L78
• lemma seedFlat_4 L79
• lemma seedFlat_5 L80
• lemma seedFlat_6 L81
• lemma seedFlat_7 L82
• lemma seedFlat_8 L83
• lemma seedFlat_9 L84
• def seedFlatMaskNat L88
• lemma seedFlat_eq_cast L92
• def maskWeight L99
• theorem seedFlatSqEdges_simplex0 L105
• theorem seedFlatSqEdges_simplex1 L112
• def hingeGramDet L122
• def apexDotNum L127
• def apex3NormSqNum L136
• def apex4NormSqNum L143
• def apexDot L149
• def apex3NormSq L150
• def apex4NormSq L151
• def cosDihedral L154
• theorem cos_numForm L159
• theorem hingeGramDet_flat L179
• theorem apexDotNum_flat L182
• theorem apex3NormSqNum_flat L185
• theorem apex4NormSqNum_flat L188
• theorem cosDihedral_flat L192
• theorem cosDihedral_flat_sq L205
• theorem cosDihedral_flat_pos L210
• theorem sinDihedral_flat L214
• def cosDihedralKernel L223
• lemma cosDihedralKernel_eight L228
• lemma cosDihedralKernel_nine L229
• lemma cosDihedralKernel_le_seven L231
• def coordPath L236
• lemma hasDerivAt_quadPoly L246
• lemma hasDerivAt_numForm L258
• lemma hasDerivAt_slot L301
• lemma path0_polys L331
• lemma path1_polys L341
• lemma path2_polys L351
• lemma path3_polys L361
• lemma path4_polys L371
• lemma path5_polys L381
• lemma path6_polys L391
• lemma path7_polys L401
• lemma path8_polys L411
• lemma path9_polys L421
• theorem hasDerivAt_cosDihedral_slot0 L433
• theorem hasDerivAt_cosDihedral_slot1 L441
• theorem hasDerivAt_cosDihedral_slot2 L449
• theorem hasDerivAt_cosDihedral_slot3 L456
• theorem hasDerivAt_cosDihedral_slot4 L463
• theorem hasDerivAt_cosDihedral_slot5 L471
• theorem hasDerivAt_cosDihedral_slot6 L478
• theorem hasDerivAt_cosDihedral_slot7 L485
• theorem hasDerivAt_cosDihedral_slot8 L492
• theorem hasDerivAt_cosDihedral_slot9 L500
• theorem hasDerivAt_cosDihedral_coord L510
• def angleKernel L528
• def singleSimplexDeficitKernel L532
• theorem angleKernel_eight L534
• theorem angleKernel_nine L541
• theorem singleSimplexDeficitKernel_eight L548
• theorem singleSimplexDeficitKernel_nine L554
• theorem singleSimplexDeficitKernel_le_seven L560
• lemma sum_fin10_split L566
• def assembleClassKernel L581
• def partialDeficitClassKernel L586
• theorem assembleClassKernel_eval L592
• theorem partialDeficitClassKernel_three L601
• theorem partialDeficitClassKernel_seven L612
• theorem partialDeficitClassKernel_eleven L623
• theorem partialDeficitClassKernel_zero_off L635
• theorem partialDeficitClassKernel_values L649
• theorem cosDihedralKernel_nonvacuous L659

… and 7 more