theorem cesGeneralHessianQF_eq_neg_variance
    (ρ F : ℝ) (P x v : Fin J → ℝ)
    (hx : ∀ j, x j ≠ 0) :
    cesGeneralHessianQF ρ F P x v =
      -(1 - ρ) * F *
        ((∑ k, P k * (v k / x k) ^ 2) -
         (∑ k, P k * (v k / x k)) ^ 2) := by
  unfold cesGeneralHessianQF cesGeneralHessianEntry
  -- Rewrite each H_{ij} v_i v_j in terms of w_j = v_j/x_j
  have h_entry : ∀ i j : Fin J,
      (if i = j then
        F * (1 - ρ) * P i * (P i - 1) / (x i) ^ 2
      else
        F * (1 - ρ) * P i * P j / (x i * x j)) *
        v i * v j =
      F * (1 - ρ) *
        ((P i * P j - if i = j then P i else 0) *
          (v i / x i) * (v j / x j)) := by
    intro i j
    split_ifs with h
    · subst h; field_simp
    · field_simp; ring
  simp_rw [h_entry]
  -- Pull F(1-ρ) out of the double sum
  have pull_const : ∀ (c : ℝ) (f : Fin J → Fin J → ℝ),
      ∑ i : Fin J, ∑ j : Fin J, c * f i j =
      c * ∑ i : Fin J, ∑ j : Fin J, f i j := by
    intro c f
    simp_rw [← Finset.mul_sum]
  rw [pull_const]
  rw [multinomial_qf P (fun j => v j / x j)]
  ring

theorem cesGeneralHessianQF_neg_semidef
    {ρ : ℝ} (hρ : ρ < 1) {F : ℝ} (hF : 0 < F)
    (P : Fin J → ℝ)
    (hP_nn : ∀ j, 0 ≤ P j)
    (hP_sum : ∑ j, P j = 1)
    (x v : Fin J → ℝ) (hx : ∀ j, x j ≠ 0) :
    cesGeneralHessianQF ρ F P x v ≤ 0 := by
  rw [cesGeneralHessianQF_eq_neg_variance ρ F P x v hx]
  have hvar := weighted_variance_nonneg P
    (fun j => v j / x j) hP_nn hP_sum
  have h1 : 0 < (1 - ρ) * F := mul_pos (by linarith) hF
  nlinarith

theorem effectiveCurvature_at_symmetry (hJ : 0 < J) (ρ : ℝ) :
    effectiveCurvatureAt ρ
      (fun _ : Fin J => (1 : ℝ) / ↑J) =
      curvatureK J ρ := by
  unfold effectiveCurvatureAt escortHerfindahl curvatureK
  simp only [Finset.sum_const, Finset.card_fin,
    nsmul_eq_mul]
  have hJne : (↑J : ℝ) ≠ 0 :=
    Nat.cast_ne_zero.mpr (by omega)
  field_simp

theorem effectiveCurvature_decreasing {ρ : ℝ} (hρ : ρ < 1)
    (P₁ P₂ : Fin J → ℝ)
    (hH : escortHerfindahl P₁ < escortHerfindahl P₂) :
    effectiveCurvatureAt ρ P₂ < effectiveCurvatureAt ρ P₁ := by
  unfold effectiveCurvatureAt
  have h1 : 0 < 1 - ρ := by linarith
  nlinarith

theorem tangentSpace_is_onePerp (hJ : 0 < J) (v : Fin J → ℝ) :
    (1 / (↑J : ℝ)) * vecSum J v = 0 ↔ orthToOne J v := by
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  simp only [orthToOne]
  constructor
  · intro h; simpa [mul_eq_zero, Nat.cast_ne_zero.mpr (by omega : J ≠ 0)] using h
  · intro h; rw [h, mul_zero]

theorem isoquant_umbilic (J : ℕ) (ρ c : ℝ) (v : Fin J → ℝ) :
    secondFundamentalFormQF J ρ c v =
    cesPrincipalCurvature J ρ c * vecNormSq J v := rfl

theorem arc_ge_chord (_hJ : 2 ≤ J) {ρ : ℝ} (_hρ : ρ < 1) {c : ℝ} (_hc : 0 < c)
    (_x _y : Fin J → ℝ) :
    -- geodesicDistSq ≥ chordalDistSq (schematic: geodesic distance not defined)
    0 ≤ sectionalCurvature J ρ c :=
  sectionalCurvature_nonneg ρ c