Documentation

Lean 4 Proof

theorem convergence_speed_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