lemma proved wrapper

`Jlog_zero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 231@[simp] lemma Jlog_zero : Jlog 0 = 0 := by

One-line wrapper that applies simp.

 232  simp [Jlog, Jcost]
 233

From the project-wide theorem graph. These declarations reference this one in their body.

EL_global_min in IndisputableMonolith.Cost decl_use
Jlog_eq_zero_iff in IndisputableMonolith.Cost decl_use
Jlog_zero in IndisputableMonolith.Cost.Jlog decl_use
jcost_kl_same_second_order_at_equilibrium in IndisputableMonolith.Information.FEPBridgeFromJCost decl_use

Lean names referenced from this declaration's body.