Documentation

Lean 4 Proof

theorem logCesEigenvaluePerp_neg {ρ : ℝ} (hρ : ρ < 1) (hJ : 0 < J)
    {c : ℝ} (hc : 0 < c) :
    logCesEigenvaluePerp J ρ c < 0 := by
  simp only [logCesEigenvaluePerp]
  apply div_neg_of_neg_of_pos
  · linarith
  · apply mul_pos (Nat.cast_pos.mpr hJ |>.trans_le le_rfl)
    positivity

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Appendix.lean:56

Module Section

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

In the same file