Documentation

Lean 4 Proof

theorem flow_decline_while_stock_rises
    {F_peak F_current : ℝ} (hpos : 0 < F_current) (hdecline : F_current < F_peak) :
    -- Flow is declining AND stock is still rising
    0 < F_current ∧ F_current < F_peak :=
  ⟨hpos, hdecline⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:145

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file