Convergence Speed Increasing Sigma

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem convergenceSpeed_increasing_sigma {sigma1 sigma2 eps : ℝ}
    (heps : 0 < eps) (h12 : sigma1 < sigma2) :
    sigma1 / eps < sigma2 / eps :=
  div_lt_div_of_pos_right h12 heps

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:29

Module Section

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

In the same file

convergence_speed_increasing_sigma equilibriumOutput_decreasing_sigma equilibrium_output_decreasing_sigma damping_cancellation_algebraic welfare_independent_of_own_sigma upstream_reform_beta upstream_reform_sigma_prev fastest_layer_regulation welfare_ordering rigidity_ordering cascade_long_run_zero hump_long_run_zero