def cesFun (J : ℕ) (a : Fin J → ℝ) (ρ : ℝ) : (Fin J → ℝ) → ℝ :=
  fun x => (∑ j : Fin J, a j * (x j) ^ ρ) ^ (1 / ρ)

def curvatureK (J : ℕ) (ρ : ℝ) : ℝ := (1 - ρ) * (↑J - 1) / ↑J

def symmetricPoint (J : ℕ) (c : ℝ) : Fin J → ℝ := fun _ => c

theorem curvatureK_pos {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) :
    0 < curvatureK J ρ := by
  simp only [curvatureK]
  apply div_pos
  · apply mul_pos
    · linarith
    · have hJ1 : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
      linarith
  · exact_mod_cast (by omega : 0 < J)