Documentation

Lean 4 Proof

theorem qCovariance_eigenstructure (J : ℕ) (q T c : ℝ) (hq : 0 < q) (hT : 0 < T)
    (hc : 0 < c) :
    -- Cov_q eigenvalue on 1⊥ = T · J · c² / ((1-q)(1-T/T*))
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:94

Module Section

Theorems 5-7, Corollaries 2-4, Propositions 8-11:

In the same file