Documentation

Lean 4 Proof

theorem qFriction_bound :
    -- T ≥ Var_q(ε) / (2 · LSE_q)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:191

Module Section

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

In the same file