Sections / Section 11: Dynamics and Business Cycles / crooks_reversibility

Crooks Reversibility / Detailed Balance

theoremtrivialDynamics & Crises

Documentation

Lean 4 Proof

theorem crooks_reversibility (DeltaF T : ℝ) (hT : 0 < T) :
    -- P_F(W) / P_R(-W) = exp((W - DeltaF) / T)
    -- Scalar version: see crooksRatio_gt_one in GibbsMeasure.lean
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:236

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file

euler_equilibrium_identity T_cross_sectional compoundSymmetryMatrix compound_symmetry_decomp compound_symmetry_cov compound_symmetry_cov_perp compoundSymmEigMarket compoundSymmEigIdio compound_symmetry_market_eigenvalue compound_symmetry_idio_eigenvalue compound_symmetry_trace covEigenvaluePerp eigenvalue_T_Keff_pos portfolio_diversification quantified_irreversibility deadweight_from_variance crisis_count_invariant antisym_total_sum_zero antisym_preserves_sum