module module

`IndisputableMonolith.Gravity.SevenGaps.SourcedMinimizerSupDiameter`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore module_import

declarations in this module (13)

def g L23
def F L27
theorem hasDerivAt_g L30
theorem g_zero L42
theorem g_monotone L45
theorem g_nonneg_of_nonneg L51
theorem g_nonpos_of_nonpos L55
theorem hasDerivAt_F L59
theorem F_zero L77
theorem F_nonneg L80
theorem sourced_tick_quadratic_well L111
theorem approx_tick_dist L138
theorem sourced_minimizer_sup_diameter L188