Documentation

Lean 4 Proof

theorem qVariance_response (J : ℕ) (q T : ℝ) (hq : 0 < q) (hT : 0 < T)
    (ε : Fin J → ℝ) :
    -- ∂p*/∂ε = (1/T) · Cov_q(ε)
    -- where Cov_q is the q-escort covariance matrix
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:46

Module Section

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

In the same file