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

hebbian_sign_structure

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)

 210theorem hebbian_sign_structure (r : ℝ) (hr : 0 < r) :
 211    (Jcost r = 0 ↔ r = 1) ∧ (r ≠ 1 → 0 < Jcost r) := by

proof body

Tactic-mode proof.

 212  constructor
 213  · constructor
 214    · intro h
 215      -- J(r) = (r-1)²/(2r) = 0 iff r = 1
 216      have heq := Jcost_eq_sq (ne_of_gt hr)
 217      rw [heq] at h
 218      have hden : (2 * r) ≠ 0 := by positivity
 219      have h0 : (r - 1) ^ 2 = 0 := by
 220        by_contra hne
 221        have : 0 < (r - 1) ^ 2 / (2 * r) := div_pos (by positivity) (by positivity)
 222        linarith
 223      nlinarith [sq_nonneg (r - 1)]
 224    · intro h; subst h; exact Jcost_unit0
 225  · exact Jcost_pos_away_from_one r hr
 226
 227/-- J-cost is minimized at r = 1 (balanced firing rates). -/

depends on (12)

Lean names referenced from this declaration's body.