Documentation

Lean 4 Proof

theorem J_mediated_activation_linearity
    {beta_n sigma_n J_n Fbar_n sigma_prev alpha : ℝ}
    (hsp : sigma_prev ≠ 0) :
    ngmEntryReal beta_n sigma_n (alpha * J_n) Fbar_n sigma_prev =
    alpha * ngmEntryReal beta_n sigma_n J_n Fbar_n sigma_prev :=
  ngmEntryReal_linear_in_J hsp

Dependency Graph

Location

thesis/CESProofs/Dynamics/HierarchicalJ.lean:34

Module Section

Paper 3c, Section 6: Hierarchical Implications

In the same file