IndisputableMonolith.Geometry.ReggeActionNonlinearCorrespondence

declarations in this module (19)

• def jCostLog L32
• theorem jCostLog_eq_cosh_sub_one L35
• theorem jCostLog_neg L40
• def weightedJCostAction L48
• theorem weightedJCostAction_neg L54
• theorem weightedJCostAction_along_line_even L71
• def canonicalJQuadraticTerm L88
• theorem canonicalJQuadraticTerm_eq_dirichlet L93
• theorem canonicalJQuadraticTerm_nonneg L101
• theorem nonlinearRegge_exact_canonical_split L110
• def NonlinearReggeJCostLocalCorrespondence L123
• def StrongestTrueReggeJCostReplacement L138
• theorem strongestTrueReggeJCostReplacement_iff_localCorrespondence L142
• theorem nonlinearRegge_localCorrespondence_of_cubicBound L148
• theorem nonlinearRegge_localCorrespondence_of_taylorTheorem L159
• theorem nonlinearRegge_localCorrespondence_of_localHessianTaylorInputs L165
• theorem nonlinearRegge_localCorrespondence_of_eventuallyZero_edgeStencil_and_taylor L173
• theorem strongestTrueReggeJCostReplacement_of_eventuallyZero_edgeStencil_and_taylor L186
• theorem nonlinearRegge_localCorrespondence_of_remainder_identically_zero L198