module module

`IndisputableMonolith.Gravity.LatticeConvergence`

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

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

IndisputableMonolith.Gravity.CubicReggeProof module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.ContinuumLimit module_import

declarations in this module (12)

def D_spatial L37
abbrev LatticeField3 L40
theorem D3_laplacian_three_terms L43
def axis_second_diff L54
theorem lattice_laplacian_is_sum_of_1D L59
def scaled_lattice_laplacian L68
theorem scaled_laplacian_sign L73
theorem lattice_laplacian_3D_convergence L90
theorem convergence_is_second_order L100
theorem jcost_neighbor_approximation_3D L108
structure LatticeConvergenceCert L121
theorem lattice_convergence_cert L131