theorem
proved
jcost_variational_minimum
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.CalculusVariationsFromRS on GitHub at line 31.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
28theorem variationalProblemCount : Fintype.card VariationalProblem = 5 := by decide
29
30/-- J-cost minimum: J = 0 at r = 1. -/
31theorem jcost_variational_minimum : Jcost 1 = 0 := Jcost_unit0
32
33/-- J-cost is strictly below off-equilibrium: J > 0 for r ≠ 1. -/
34theorem jcost_off_minimum {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
35 0 < Jcost r := Jcost_pos_of_ne_one r hr hne
36
37structure VariationsCert where
38 five_problems : Fintype.card VariationalProblem = 5
39 minimum_at_1 : Jcost 1 = 0
40 off_minimum_positive : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
41
42def variationsCert : VariationsCert where
43 five_problems := variationalProblemCount
44 minimum_at_1 := jcost_variational_minimum
45 off_minimum_positive := jcost_off_minimum
46
47end IndisputableMonolith.Mathematics.CalculusVariationsFromRS