IsWithinHorizon

formal source

  55def IsPastHorizon (r : ℝ) : Prop := PredictabilityThreshold ≤ forecastCost r
  56
  57/-- Forecast is within the horizon iff its J-cost is strictly below. -/
  58def IsWithinHorizon (r : ℝ) : Prop := forecastCost r < PredictabilityThreshold
  59
  60theorem horizon_states_exclusive {r : ℝ} :
  61    ¬ (IsWithinHorizon r ∧ IsPastHorizon r) := by
  62  rintro ⟨h_lt, h_ge⟩
  63  exact (lt_irrefl _) (lt_of_lt_of_le h_lt h_ge)
  64
  65theorem predictability_threshold_band :
  66    0.11 < PredictabilityThreshold ∧ PredictabilityThreshold < 0.13 := by
  67  unfold PredictabilityThreshold
  68  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  69  rw [Cost.Jcost_eq_sq hphi_ne]
  70  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  71  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  72  have hpos : (0 : ℝ) < 2 * phi := by
  73    have : (0 : ℝ) < phi := Constants.phi_pos
  74    linarith
  75  refine ⟨?lo, ?hi⟩
  76  · rw [lt_div_iff₀ hpos]
  77    nlinarith [h_lo, h_hi]
  78  · rw [div_lt_iff₀ hpos]
  79    nlinarith [h_lo, h_hi]
  80
  81structure ClimatePredictabilityCert where
  82  unit_zero : forecastCost 1 = 0
  83  reciprocal_symm :
  84    ∀ {r : ℝ}, 0 < r → forecastCost r = forecastCost r⁻¹
  85  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ forecastCost r
  86  threshold_band :
  87    0.11 < PredictabilityThreshold ∧ PredictabilityThreshold < 0.13
  88  states_exclusive :