Documentation

Lean 4 Proof

theorem upstream_reform_sigma_prev {sigma_prev1 sigma_prev2 delta beta : ℝ}
    (hdelta : delta ≠ 0) (hb : 0 < beta) (h12 : sigma_prev1 < sigma_prev2) :
    welfareContribution sigma_prev1 delta beta <
    welfareContribution sigma_prev2 delta beta := by
  simp only [welfareContribution]
  apply div_lt_div_of_pos_right _ hb
  exact mul_lt_mul_of_pos_right h12 (sq_pos_of_ne_zero hdelta)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:101

Module Section

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

In the same file