Potential Is Stable of strong

lemma potentialIsStable_of_strong (P : PotentialParameters)    (h : ∀ k, ‖k‖ ^ 2 ≤ 1 → 0 < quarticTermReduced P k) :    PotentialIsStable P := by  rw [potentialIsStable_iff_massTermReduced_sq_le_quarticTermReduced]  let S := Metric.closedBall (0 : EuclideanSpace ℝ (Fin 3)) 1  have S_nonEmpty : S.Nonempty := ⟨0, by simp [S]⟩  obtain ⟨kmax, kmax_S, kmax_isMax⟩ := IsCompact.exists_isMaxOn    (isCompact_closedBall 0 1) S_nonEmpty    (f := fun k => (massTermReduced P k ^ 2) / (4 * quarticTermReduced P k)) <| by    apply ContinuousOn.div₀    · simp only [massTermReduced, Fin.isValue]      fun_prop    · simp only [quarticTermReduced, Fin.isValue]      fun_prop    · intro x hx      specialize h x (by simpa using hx)      linarith  use (massTermReduced P kmax) ^ 2 / (4 * quarticTermReduced P kmax)  apply And.intro  · refine (le_div_iff₀ ?_).mpr ?_    · specialize h kmax (by simpa using kmax_S)      linarith    · simp only [zero_mul]      exact sq_nonneg (massTermReduced P kmax)  · intro k hk    apply And.intro    · specialize h k hk      linarith    · intro hq      rw [isMaxOn_iff] at kmax_isMax      refine (div_le_iff₀' ?_).mp (kmax_isMax k (by simpa using hk))      grind