`JcostN_reciprocal`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.Ndim.Core
domain: Cost
line: 127 · 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 127.

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.

open explainer

depends on

formal source

 124          simp
 125
 126/-- Reciprocity under componentwise inversion. -/
 127theorem JcostN_reciprocal {n : ℕ} (α x : Vec n) :
 128    JcostN α (hadamardInv x) = JcostN α x := by
 129  rw [JcostN_eq_cosh_logsum, JcostN_eq_cosh_logsum]
 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.