  88  rw [hrewrite] at hε
  89  nlinarith [sq_nonneg (2 * C + 3)]
  90
  91structure CostFirstExistenceCert where
  92  rsExists_iff : ∀ {x : ℝ}, 0 < x → (RSExists x ↔ x = 1)
  93  non_existence_costly :
  94    ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
  95  nothing_diverges :
  96    ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C
  97
  98/-- Cost-first existence certificate. -/
  99def costFirstExistenceCert : CostFirstExistenceCert where
 100  rsExists_iff := @rsExists_iff_one
 101  non_existence_costly := @non_existence_has_positive_cost
 102  nothing_diverges := divergence_at_zero_direction
 103
 104end
 105end CostFirstExistence
 106end Foundation
 107end IndisputableMonolith

papers checked against this theorem

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