module module

`IndisputableMonolith.Cost.Derivative`

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.Cost module_import

declarations in this module (10)

lemma differentiableAt_Jcost L29
lemma deriv_Jcost_eq L46
def linJ L72
lemma linJ_unit L75
theorem linJ_eq_derivative_times_x L81
def remJ L105
lemma remJ_unit L113
lemma Jcost_exp_nonneg L118
theorem linJ_matches_harm_def L128
theorem harm_linearization_correct L134