pith. machine review for the scientific record. sign in
theorem proved term proof

JcostN_reciprocal

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 127theorem JcostN_reciprocal {n : ℕ} (α x : Vec n) :
 128    JcostN α (hadamardInv x) = JcostN α x := by

proof body

Term-mode proof.

 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. -/

depends on (7)

Lean names referenced from this declaration's body.