lemma proved term proof

`Jlog_zero`

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

formal statement (Lean)

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

Term-mode proof.

  12  simp [Jlog]
  13
  14open Complex
  15

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 decl_use
jcost_kl_same_second_order_at_equilibrium in IndisputableMonolith.Information.FEPBridgeFromJCost decl_use

Lean names referenced from this declaration's body.