Documentation

Lean 4 Proof

theorem financial_real_lag_increases
    {r1 r2 : ℝ} (hr1 : 0 < r1) (hle : r1 ≤ r2)
    {v : ℝ} (hv : 0 < v) :
    v / r2 ≤ v / r1 :=
  timescaleGap_monotone_in_relaxRate hr1 hle hv

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:368

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file