theorem lemma2_1 (n : ℕ) (speedvec : PiLp 1 fun (x : Fin n) => ℝ) (cN : PiLp 1 fun (x : Fin n) => ℕ) (cR : PiLp 1 fun (x : Fin n) => ℝ) (s : (PiLp 1 fun (x : Fin n) => ℝ) → ℝ) (h : SpeedUpFunction n speedvec cN s) (h₂ : ∀ (i : Fin n), ↑(cN i) = cR i) (i : ℝ) : i ≠ 0 → i < ‖cR‖ → ∃ ε > 0, i * s ((1 / i) • cR) < (i + ε) * s ((1 / (i + ε)) • cR) ∧ ∀ (i : ℝ), i ≠ 0 → i ≥ ‖cR‖ → ∀ ε > 0, i * s ((1 / i) • cR) ≤ (i + ε) * s ((1 / (i + ε)) • cR)