module
module
IndisputableMonolith.Gravity.ReggeCubicLatticeLimit
show as:
view Lean formalization →
used by (1)
depends on (2)
declarations in this module (10)
-
structure
RegularCubicLatticeModel -
def
ReggeSecondOrderCubicLatticeLimit -
structure
ReggeCubicLatticeLimitInput -
structure
PhysicalSixTetCubicDirichletModel -
def
cubicLatticeLimitInput_of_physicalSixTetModel -
theorem
reggeActionSecondOrder_cubic_lattice_limit -
theorem
reggeSecondOrderCubicLatticeLimit_error_vanishes_along_models -
theorem
finite_difference_second_order_estimate -
def
exactSecondOrderComparisonModel -
def
exactSecondOrderCubicLatticeLimitInput