referenceHorizon

formal source

  36
  37/-- Reference forecast horizon (RS-native dimensionless 1, calibrated
  38at ECMWF rung 0). -/
  39def referenceHorizon : ℝ := 1
  40
  41/-- Forecast horizon at φ-ladder rung `k` (negative `k` for lower-
  42resolution model that loses skill earlier; we work with positive `k`
  43and flip sign in the bridge theorem below). -/
  44def horizonAtRung (k : ℕ) : ℝ := referenceHorizon * phi ^ (-(k : ℤ))
  45
  46theorem horizonAtRung_pos (k : ℕ) : 0 < horizonAtRung k := by
  47  unfold horizonAtRung referenceHorizon
  48  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  49  linarith [this]
  50
  51theorem horizonAtRung_succ_ratio (k : ℕ) :
  52    horizonAtRung (k + 1) = horizonAtRung k * phi⁻¹ := by
  53  unfold horizonAtRung
  54  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  55  have hzpow : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  56    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  57    rw [zpow_add₀ hphi_ne]
  58    simp
  59  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  60  rw [hcast, hzpow]; ring
  61
  62theorem horizonAtRung_strictly_decreasing (k : ℕ) :
  63    horizonAtRung (k + 1) < horizonAtRung k := by
  64  rw [horizonAtRung_succ_ratio]
  65  have hk : 0 < horizonAtRung k := horizonAtRung_pos k
  66  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  67    have hphi_gt_one : (1 : ℝ) < phi := by
  68      have := Constants.phi_gt_onePointFive; linarith
  69    exact inv_lt_one_of_one_lt₀ hphi_gt_one