Documentation

Lean 4 Proof

theorem jarzynski_equality (DeltaF T : ℝ) (hT : 0 < T) :
    -- <exp(-W/T)> = exp(-DeltaF/T)
    -- where the average is over all possible policy implementation paths
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:42

Module Section

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

In the same file