Documentation

Lean 4 Proof

theorem quantified_irreversibility {W DeltaF T : ℝ}
    (hT : 0 < T) (hW : 0 < W) (hDF : DeltaF < 0) :
    Real.exp ((W - DeltaF) / T) > 1 := by
  rw [gt_iff_lt]
  exact Real.one_lt_exp_iff.mpr (div_pos (by linarith) hT)

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:254

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file