Mass Metric Val is Von NBounded

lemma massMetricVal_isVonNBounded    (S : HarmonicOscillator) (q : ConfigurationSpace) :    IsVonNBounded ℝ      {v : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) q | massMetricVal S q v v < 1} := by  change IsVonNBounded ℝ    {v : EuclideanSpace ℝ (Fin 1) | S.m * ⟪v, v⟫_ℝ < 1}  rw [NormedSpace.isVonNBounded_iff']  refine ⟨Real.sqrt (1 / S.m), ?_⟩  intro v hv  have hv' : S.m * ⟪v, v⟫_ℝ < 1 := by simpa using hv  rw [real_inner_self_eq_norm_sq] at hv'  have hmul : S.m * ‖v‖ ^ 2 < 1 := hv'  have hsq_le : ‖v‖ ^ 2 ≤ 1 / S.m := by    have hsq_lt : ‖v‖ ^ 2 < 1 / S.m := by      rw [lt_div_iff₀ S.m_pos]      nlinarith [hmul]    exact hsq_lt.le  exact Real.le_sqrt_of_sq_le hsq_le