module module

`IndisputableMonolith.Gravity.SevenGaps.StrainDescent`

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.SevenGaps.DescentPrincipleUniversality module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore module_import

declarations in this module (36)

def sourceCost1 L83
def strainResidual L86
def strainEnvelope L91
def strainStepSize L97
def strainStep1 L100
theorem strainEnvelope_ge_one L103
theorem strainEnvelope_pos L108
theorem strainStepSize_pos L112
theorem strainStepSize_le_one L117
theorem cosh_le_cosh_of_nonneg_of_le L124
theorem integral_sinh L142
theorem integral_cosh L150
theorem sinh_le_mul_cosh L159
theorem integral_id_half_sq L173
theorem integral_sq_half_third L185
theorem cosh_sub_one_le_sq_half_cosh L197
theorem abs_sinh_sub_self_le_sixth L229
theorem step_one_dim_sub L309
theorem cosh_step_le_cosh_abs_residual L320
theorem correction_le_half L336
theorem descent_one_dim L435
theorem descent_one_dim_lt L443
theorem step_fixed_iff_arsinh L458
theorem abs_sinh_eq_sinh_abs L480
theorem contraction_one_dim L493
def strainOrbit L604
theorem strainOrbit_abs_le L609
theorem strainOrbit_tendsto L726
def strainStepVec L741
theorem sourcedAction_eq_sum_sourceCost1 L745
theorem sourcedAction_step_le L751
theorem sourcedAction_step_lt L767
theorem stepVec_fixed_iff_minimizer L788
def strainStepVecOrbit L801
theorem strainStepVecOrbit_apply L807
theorem strainStepVec_tendsto_minimizer L818