Documentation

Lean 4 Proof

theorem rigidity_ordering {eps1 eps2 W1 W2 : ℝ}
    (heps : eps2 < eps1) (hW : W2 < W1)
    (_heps2 : 0 < eps2) (hW2 : 0 < W2) :
    eps2 * W2 < eps1 * W1 :=
  calc eps2 * W2 < eps1 * W2 := mul_lt_mul_of_pos_right heps hW2
    _ ≤ eps1 * W1 := mul_le_mul_of_nonneg_left (le_of_lt hW) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:151

Module Section

Proposition 6, Theorem 9, Corollaries 1-2 and 4:

In the same file