module module

`IndisputableMonolith.Gravity.ReggeConvergence`

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 (4)

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

IndisputableMonolith.Gravity.CubicReggeConvergence module_import
IndisputableMonolith.Gravity.CubicReggeProof module_import
IndisputableMonolith.Gravity.FullEFE module_import
IndisputableMonolith.Gravity.UnifiedLatticeManifoldCorrespondence module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.ContinuumLimit module_import
IndisputableMonolith.Gravity.ReggeCalculus module_import
IndisputableMonolith.Gravity.RicciTensor module_import

declarations in this module (11)

def linearized_convergence_proved L59
theorem linearized_error_estimate L65
theorem linearized_convergence L78
structure CMSConditions L91
def nonlinear_convergence_with_conditions L102
def cubic_shape_bound L109
theorem cubic_shape_optimal L111
def rs_regge_convergence L118
def weak_field_covers L135
structure ReggeConvergenceCert L144
theorem regge_convergence_cert L149