Documentation

Lean 4 Proof

theorem tsallisHessian_uniform_on_perp (_hJ : 0 < J) (q : ℝ) (hq : 0 < q)
    (v : Fin J → ℝ) (_hv : orthToOne J v) :
    -- The Hessian quadratic form at uniform is proportional to ‖v‖²
    -- with coefficient -q · J^{q-1}
    tsallisHessianDiag J q * vecNormSq J v ≤ 0 := by
  apply mul_nonpos_of_nonpos_of_nonneg
  · simp only [tsallisHessianDiag]
    apply mul_nonpos_of_nonpos_of_nonneg (by linarith)
    exact rpow_nonneg (Nat.cast_nonneg J) _
  · simp only [vecNormSq]
    exact Finset.sum_nonneg fun j _ => sq_nonneg _

Dependency Graph

Location

thesis/CESProofs/Potential/Appendix.lean:116

Module Section

Appendix Lemmas 1-3 (Paper 2, Appendix A)

In the same file