Documentation

Lean 4 Proof

theorem welfare_ordering {W1 W2 P sigma beta1 beta2 : ℝ}
    (hP : 0 < P) (hs : 0 < sigma) (hb1 : 0 < beta1) (_hb2 : 0 < beta2)
    (hbeta : beta1 < beta2)
    (hW1 : W1 = P / (sigma * beta1))
    (hW2 : W2 = P / (sigma * beta2)) :
    W2 < W1 := by
  rw [hW1, hW2]
  exact div_lt_div_of_pos_left hP (mul_pos hs hb1) (mul_lt_mul_of_pos_left hbeta hs)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:134

Module Section

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

In the same file