Documentation

Lean 4 Proof

theorem administered_slower {v_price sigma : ℝ}
    (hv : 0 < v_price) (hsigma : 0 < sigma) :
    administeredSpeed v_price sigma < v_price := by
  simp only [administeredSpeed]
  exact div_lt_self hv (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:179

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file