Cost.Jlog
IndisputableMonolith.Cost.Jlog
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
From the project-wide theorem graph. These declarations reference this one in their body.
IndisputableMonolith.LedgerPostingAdjacency
Jlog
Jlog_as_exp
Jlog_zero
Jlog_eq_cosh_sub_one
Jlog_nonneg
Jlog_pos_iff
Jlog_eq_zero_iff
Jlog_strictMonoOn_Ici0