IndisputableMonolith.Cost.SymplecticAction

declarations in this module (25)

• def areaForm L84
• theorem areaForm_mulVec L87
• def ConservesSigma L97
• def sigmaAreaDefect L100
• theorem conservesSigma_iff_defect_zero L102
• theorem conservesSigma_iff_preservesArea L109
• theorem ledger_adjugate_sum L127
• theorem trace_mul_add_trace_mul_adjugate L138
• theorem trace_identity_of_conservesSigma L152
• theorem reciprocal_eigenvalue_pairing L165
• def diagSL L174
• theorem diagSL_trace L176
• theorem diagSL_det L179
• theorem diagSL_conservesSigma L182
• def traceCost L187
• theorem traceCost_diagSL L191
• theorem jcost_exp_eq_cosh_sub_one L198
• theorem trace_diagSL_mul L204
• theorem trace_diagSL_mul_inv L208
• theorem split_torus_trace_identity L218
• theorem rcl_from_symplectic_action L229
• theorem jcost_satisfiesCompositionLaw_via_symplectic L248
• theorem jcost_forced_by_symplectic_action L258
• structure SymplecticActionCert L276
• theorem symplecticActionCert L298