Documentation

Lean 4 Proof

theorem friction_work_estimate (VarW T : ℝ) (hT : 0 < T) :
    -- W_diss ~ Var(W) / (2T) to leading order
    -- (Gaussian approximation of the Jarzynski equality)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:116

Module Section

Results 26-35: Minimum Policy Cost and Multi-Scale Aggregation

In the same file