theorem
proved
global_minimum
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.OptimizationTheoryFromRS on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
28theorem optimizationProblemTypeCount : Fintype.card OptimizationProblemType = 5 := by decide
29
30/-- Global minimum: J = 0. -/
31theorem global_minimum : Jcost 1 = 0 := Jcost_unit0
32
33/-- Local minimum: J > 0. -/
34theorem local_minimum {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
35 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
36
37structure OptimizationTheoryCert where
38 five_types : Fintype.card OptimizationProblemType = 5
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