Documentation

Lean 4 Proof

theorem tsallisHessianDiag_neg (hJ : 0 < J) {q : ℝ} (hq : 0 < q) :
    tsallisHessianDiag J q < 0 := by
  simp only [tsallisHessianDiag]
  apply mul_neg_of_neg_of_pos (by linarith)
  exact rpow_pos_of_pos (Nat.cast_pos.mpr hJ) _

Dependency Graph

Location

thesis/CESProofs/Potential/Appendix.lean:129

Module Section

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

In the same file