module module

`IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.WeightedHypersurfaceBracket module_import

declarations in this module (65)

abbrev PhaseSpace L106
def coordQ L111
def coordP L115
lemma coordQ_apply L119
lemma coordP_apply L122
def pderivQ L128
def pderivP L133
def bracket L141
lemma sum_shift L147
lemma sum_reindex L152
lemma sum_mul_ite L158
lemma sum_mul_ite_add L168
lemma sum_mul_ite_sub L184
theorem bracket_antisymm L206
theorem bracket_self L214
lemma pderivQ_fun_add L219
lemma pderivP_fun_add L224
lemma pderivQ_const_mul L229
lemma pderivP_const_mul L234
lemma pderivQ_fun_mul L239
lemma pderivP_fun_mul L244
theorem bracket_add_left L251
theorem bracket_add_right L259
theorem bracket_const_mul_left L269
theorem bracket_const_mul_right L276
theorem bracket_mul_left L286
theorem bracket_mul_right L294
def JacobiOn L307
lemma hasFDerivAt_coord_fst L313
lemma hasFDerivAt_coord_snd L317
theorem bracket_coordQ_coordP L322
theorem bracket_coordQ_coordQ L362
theorem bracket_coordP_coordP L376
def Dgen L398
def DgenSym L406
def Ham L411
lemma Ham_eq_sq L415
lemma DgenSym_eq L421
def DgenD L432
lemma hasFDerivAt_Dgen L436
theorem differentiable_Dgen L444
def DgenSymD L448
lemma hasFDerivAt_DgenSym L453
theorem differentiable_DgenSym L462
def HamD L466
lemma hasFDerivAt_Ham L472
theorem differentiable_Ham L482
lemma pderivQ_Dgen L487
lemma pderivP_Dgen L500
lemma pderivQ_DgenSym L511
lemma pderivP_DgenSym L527
lemma pderivP_Ham L540
lemma pderivQ_Ham L555
theorem bracket_Dgen_Dgen L584
theorem bracket_DgenSym_DgenSym L624
theorem bracket_Dgen_Ham L698
theorem bracket_Dgen_Ham_one L732
theorem bracket_DgenSym_Ham L782
theorem bracket_DgenSym_Ham_one L861
theorem bracket_Ham_one_DgenSym L867
theorem bracket_Ham_Ham L883
structure below L911
structure function L925
structure HojmanKucharTeitelboimTarget L928
def HKTRigidityStatement L971