`optimizationTheoryCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.OptimizationTheoryFromRS
domain: Mathematics
line: 42 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.OptimizationTheoryFromRS on GitHub at line 42.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  39  global_min : Jcost 1 = 0
  40  local_min : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  41
  42def optimizationTheoryCert : OptimizationTheoryCert where
  43  five_types := optimizationProblemTypeCount
  44  global_min := global_minimum
  45  local_min := local_minimum
  46
  47end IndisputableMonolith.Mathematics.OptimizationTheoryFromRS

papers checked against this theorem

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