recognition / Cost / Cost.Ndim.Core / JcostN_eq_zero_iff

theorem

`JcostN_eq_zero_iff`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.Ndim.Core
domain: Cost
line: 133 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.Ndim.Core on GitHub at line 133.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

depends on

used by

zero_cost_iff_dot_zero IndisputableMonolith.Cost.Ndim.Neutrality

formal source

 130  rw [dot_log_hadamardInv, Real.cosh_neg]
 131
 132/-- Zero-cost characterization in log coordinates. -/
 133theorem JcostN_eq_zero_iff {n : ℕ} (α x : Vec n) :
 134    JcostN α x = 0 ↔ dot α (logVec x) = 0 := by
 135  unfold JcostN JlogN
 136  simpa [Jlog] using (Jlog_eq_zero_iff (t := dot α (logVec x)))
 137
 138end Ndim
 139end Cost
 140end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.