module module

`IndisputableMonolith.Foundation.JCostGeometry`

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.Foundation.TopologicalVeto module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (23)

theorem jcost_at_one L36
theorem jcost_nonneg' L39
theorem jcost_eq_zero_iff L42
theorem jcost_reciprocal L58
theorem jcost_pos_away_from_one L63
theorem jcost_unit_curvature L68
theorem jcost_exp_eq L74
theorem jcost_squared_form L79
theorem jcost_ratio_zero_iff L85
def totalJcost L92
theorem totalJcost_nonneg L96
def geometricMean L109
theorem geometricMean_pos L113
theorem totalJcost_at_geomean_symmetric L121
def arithmeticMean L157
theorem geometric_ne_arithmetic L161
theorem simultaneous_differs_from_sequential L182
theorem rcl_identity L190
def phi L199
theorem phi_sq L202
theorem phi_pos L209
def jBit L215
theorem jBit_pos L218