module module

`IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation`

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.HKTCanonicalMomTarget module_import
IndisputableMonolith.Gravity.SevenGaps.HKTGroundworkAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation module_import

declarations in this module (17)

abbrev LocalHamProfile L21
def LocalHamFromProfile L23
structure LocalHamSmooth L27
def localCellD L39
lemma hasFDerivAt_localCell L45
def LocalHamFromProfileD L51
lemma hasFDerivAt_LocalHamFromProfile L55
theorem differentiable_LocalHamFromProfile L62
lemma cellD_pdir L67
lemma cellD_qdir L75
theorem pderivP_LocalHamFromProfile L96
theorem pderivQ_LocalHamFromProfile L112
def localHamHamCoefficient L134
theorem local_profile_ham_ham_form L139
def LocalProfileMomDensityIdentity L171
theorem localHamHamCoefficient_witnesses_identity L178
def LocalProfileHamHamFormGeneral L185