pith. machine review for the scientific record. sign in
def 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)

  92def climatePredictabilityCert : ClimatePredictabilityCert where
  93  unit_zero := forecastCost_zero_at_unit

proof body

Definition body.

  94  reciprocal_symm := forecastCost_reciprocal_symm
  95  cost_nonneg := forecastCost_nonneg
  96  threshold_band := predictability_threshold_band
  97  states_exclusive := horizon_states_exclusive
  98
  99end
 100end PredictabilityFromJCost
 101end Climate
 102end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.