Documentation

Lean 4 Proof

theorem administered_relaxTime_gt {v_price sigma : ℝ}
    (hv : 0 < v_price) (hsigma : 0 < sigma) :
    1 / v_price < 1 / administeredSpeed v_price sigma :=
  one_div_lt_one_div_of_lt (div_pos hv (by linarith)) (div_lt_self hv (by linarith))

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:186

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file