pith. machine review for the scientific record. sign in
structure definition def or abbrev

ClimatePredictabilityCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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 :
  89    ∀ {r : ℝ}, ¬ (IsWithinHorizon r ∧ IsPastHorizon r)
  90
  91/-- Climate-predictability-horizon certificate. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.