Documentation

Lean 4 Proof

theorem upstream_reform_beta {sigma_prev delta beta1 beta2 : ℝ}
    (hs : 0 < sigma_prev) (hdelta : delta ≠ 0)
    (hb1 : 0 < beta1) (_hb2 : 0 < beta2) (h12 : beta1 < beta2) :
    welfareContribution sigma_prev delta beta2 <
    welfareContribution sigma_prev delta beta1 := by
  simp only [welfareContribution]
  apply div_lt_div_of_pos_left _ hb1 h12
  exact mul_pos hs (sq_pos_of_ne_zero hdelta)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:91

Module Section

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

In the same file