Documentation

Lean 4 Proof

theorem barrier_decreases_with_T {DeltaPhi T₁ T₂ DeltaS_q : ℝ}
    (hS : 0 < DeltaS_q) (h12 : T₁ < T₂) :
    DeltaPhi - T₂ * DeltaS_q < DeltaPhi - T₁ * DeltaS_q := by
  linarith [mul_lt_mul_of_pos_right h12 hS]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:205

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file