Documentation

Lean 4 Proof

theorem curvatureK_neg_substitute (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 1 < ρ) :
    curvatureK J ρ < 0 := by
  simp only [curvatureK]
  apply div_neg_of_neg_of_pos
  · have hJ1 : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    exact mul_neg_of_neg_of_pos (by linarith) (by linarith)
  · exact Nat.cast_pos.mpr (by omega)

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:40

Module Section

Substitute Regime: The ρ > 1 Theory (Anti-Complementarity)

In the same file