theorem
proved
jcost_minimum
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.FundamentalTheoremCalculusFromRS on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
29theorem calculusTheoremCount : Fintype.card CalculusTheorem = 5 := by decide
30
31/-- J(1) = 0 (minimum, derivative = 0 at critical point). -/
32theorem jcost_minimum : Jcost 1 = 0 := Jcost_unit0
33
34/-- J is positive off minimum (strict local minimum). -/
35theorem jcost_strict_min {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
36 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
37
38structure CalculusCert where
39 five_theorems : Fintype.card CalculusTheorem = 5
40 minimum_at_1 : Jcost 1 = 0
41 strict_minimum : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
42
43def calculusCert : CalculusCert where
44 five_theorems := calculusTheoremCount
45 minimum_at_1 := jcost_minimum
46 strict_minimum := jcost_strict_min
47
48end IndisputableMonolith.Mathematics.FundamentalTheoremCalculusFromRS