hebbian_sign_structure

formal source

 207  The Hebbian covariance f_u·f_v - ⟨f_u⟩·⟨f_v⟩ is positive when firing
 208  is correlated (r ≈ 1, J ≈ 0) and negative when uncorrelated (r ≠ 1, J > 0).
 209  Thus J-cost descent ↔ Hebbian sign structure. -/
 210theorem hebbian_sign_structure (r : ℝ) (hr : 0 < r) :
 211    (Jcost r = 0 ↔ r = 1) ∧ (r ≠ 1 → 0 < Jcost r) := by
 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). -/
 228theorem Jcost_min_at_one : Jcost 1 = 0 := Jcost_unit0
 229
 230/-- J-cost is strictly positive when r ≠ 1. -/
 231theorem Jcost_pos_of_ne_one (r : ℝ) (hr : 0 < r) (hr_ne : r ≠ 1) :
 232    0 < Jcost r := by
 233  have h := Jcost_eq_sq (ne_of_gt hr)
 234  rw [h]
 235  apply div_pos
 236  · have : r - 1 ≠ 0 := sub_ne_zero.mpr hr_ne
 237    positivity
 238  · positivity
 239
 240/-! ## §5  Working Memory Capacity -/