IndisputableMonolith.Gravity.D2QuadratureInstances

declarations in this module (12)

• theorem canonicalDirichletEnergy_zero L65
• def flattenSlice L76
• theorem flattenSlice_quadratureIntegral L105
• def flatFamily L129
• theorem flatFamily_quadrature_target L139
• theorem d2_quadrature_target_flat L154
• theorem dampedFlat_fullReggeProduct_tendsto_zero L170
• def dampedFlatProductFilterData L187
• theorem dampedFlatProductFilterData_satisfies_master_target L200
• theorem quadratureIntegral_of_uniform_probe L218
• theorem quadrature_target_iff_of_proxy_eq L276
• theorem d2_flat_sector_one_statement L297