module module

`IndisputableMonolith.Cost.FlogEL`

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

def Jlog L8
lemma Jlog_eq_zero_iff L10
lemma Jlog_nonneg L15
lemma hasDerivAt_Jlog L30
class AveragingDerivation L43
def Flog L47
lemma Flog_eq_Jlog_pt L49
lemma Flog_eq_Jlog L54
lemma hasDerivAt_Flog_of_derivation L58
lemma deriv_Flog_zero_of_derivation L65
lemma Flog_nonneg_of_derivation L70
lemma Flog_eq_zero_iff_of_derivation L75
theorem T5_EL_equiv_general L80