Documentation

Lean 4 Proof

theorem relative_has_positive_K_sensitivity
    {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    0 < curvatureK J ρ :=
  curvatureK_pos hJ hρ

Dependency Graph

Location

thesis/CESProofs/Dynamics/IndicatorClassification.lean:98

Module Section

Derivation of Leading and Lagging Economic Indicators

In the same file