  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

papers checked against this theorem

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