module
module
IndisputableMonolith.Gravity.D2ScalarDirichletQuadratureLimit
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (6)
-
structure
ScalarDirichletEnergyLimit -
theorem
scalar_dirichlet_limit_implies_d2_quadrature_target -
theorem
scalar_limit_and_damped_implies_full_convergence -
def
flatFamily_scalarDirichletLimit -
theorem
flatFamily_quadrature_target_via_scalar_limit -
theorem
dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit