module module

`IndisputableMonolith.Gravity.NonlinearConvergence`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.ReggeCalculus module_import

declarations in this module (10)

def regge_to_eh_convergence_axiom L58
def regge_ricci_convergence_axiom L72
def regge_riemann_convergence_axiom L89
theorem convergence_is_second_order L98
theorem error_vanishes L102
structure RSReggeConvergence L121
def rs_implies_gr L128
def proof_requirements L150
structure NonlinearConvergenceCert L159
theorem nonlinear_convergence_cert L165