def cesPotential (J : ℕ) (q T : ℝ) (p : Fin J → ℝ) (ε : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, p j * ε j - T * tsallisEntropy J q p

def tsallisEntropy (J : ℕ) (q : ℝ) (p : Fin J → ℝ) : ℝ :=
  if q = 1 then -∑ j : Fin J, p j * Real.log (p j)
  else (1 - ∑ j : Fin J, (p j) ^ q) / (q - 1)

theorem effectiveCurvatureKeff_above_critical (J : ℕ) (ρ T Tstar : ℝ)
    (hTs : 0 < Tstar) (hT : Tstar ≤ T) :
    effectiveCurvatureKeff J ρ T Tstar = 0 := by
  simp only [effectiveCurvatureKeff]
  have h : 1 - T / Tstar ≤ 0 := by
    rw [sub_nonpos]
    rwa [le_div_iff₀ hTs, one_mul]
  rw [max_eq_left h, mul_zero]

theorem monotone_integration {T₁ T₂ Tstar₁ Tstar₂ : ℝ}
    (_hTs1 : 0 < Tstar₁) (_hTs2 : 0 < Tstar₂)
    (hT : T₁ ≤ T₂) (hTs : Tstar₂ ≤ Tstar₁) :
    -- If activity 1 is outsourced (T₁ ≥ T*₁), then activity 2 is also outsourced
    Tstar₁ ≤ T₁ → Tstar₂ ≤ T₂ := by
  intro h
  linarith