Documentation

Lean 4 Proof

theorem equilibrium_output_decreasing_sigma {sigma1 sigma2 phi_val : ℝ}
    (hphi : 0 < phi_val) (hs1 : 0 < sigma1) (_hs2 : 0 < sigma2)
    (h12 : sigma1 < sigma2) :
    phi_val / sigma2 < phi_val / sigma1 :=
  div_lt_div_of_pos_left hphi hs1 h12

Dependency Graph

Location

thesis/CESProofs/Hierarchy/DampingCancellation.lean:42

Module Section

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

In the same file