pith. machine review for the scientific record. sign in
structure

WeatherPredictabilityCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Meteorology.WeatherPredictabilityFromJCost
domain
Meteorology
line
29 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Meteorology.WeatherPredictabilityFromJCost on GitHub at line 29.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  26
  27theorem predictionRangeCount : Fintype.card PredictionRange = 5 := by decide
  28
  29structure WeatherPredictabilityCert where
  30  five_ranges : Fintype.card PredictionRange = 5
  31  skill_threshold : CanonicalCert
  32
  33noncomputable def weatherPredictabilityCert : WeatherPredictabilityCert where
  34  five_ranges := predictionRangeCount
  35  skill_threshold := cert
  36
  37end IndisputableMonolith.Meteorology.WeatherPredictabilityFromJCost

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.