module module

`IndisputableMonolith.Gravity.D2DampedScheduleClosure`

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

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

IndisputableMonolith.Gravity.D2QuadratureInstances module_import
IndisputableMonolith.Gravity.Track1BCorrectedQuadratic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.D2ScopingAudit module_import

declarations in this module (31)

theorem canonicalDirichletEnergy_smul L75
def localRadius L105
def localConstant L114
theorem localRadius_pos L122
theorem localConstant_nonneg L131
theorem local_bound L142
def probeNormSum L172
def probeCubeSum L182
theorem probeNormSum_nonneg L191
theorem probeCubeSum_nonneg L200
def residualCoefficient L211
theorem residualCoefficient_nonneg L219
def dampingFactor L230
theorem one_add_probeNormSum_pos L235
theorem one_add_residualCoefficient_pos L242
theorem dampingFactor_pos L249
theorem dampingFactor_le_radius_quotient L258
theorem dampingFactor_mul_residualCoefficient_le_one L264
def dampedSlice L284
theorem dampedSlice_quadratureIntegral L316
theorem normalized_regge_sub_limit_abs_le L330
theorem dampedSlice_residual_abs_le L434
def dampedFamily L551
theorem dampedFamily_uniformResidual L565
theorem dampedFamily_quadrature_target L588
def dampedProductFilterData L608
theorem dampedFamily_fullReggeProduct_tendsto_continuum L632
theorem dampedProductFilterData_satisfies_master_target L652
theorem d2_residual_vanishing_target_damped L674
theorem d2_reduction_to_quadrature_only L689
theorem d2_damped_schedule_closure_one_statement L709