`JcostN_reciprocal`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.