Documentation

Lean 4 Proof

theorem regime_trichotomy (hJ : 2 ≤ J) {ρ : ℝ} :
    (ρ < 1 → 0 < curvatureK J ρ) ∧
    (ρ = 1 → curvatureK J ρ = 0) ∧
    (1 < ρ → curvatureK J ρ < 0) :=
  ⟨fun hρ => curvatureK_pos hJ hρ,
   fun hρ => by rw [hρ]; exact curvatureK_eq_zero_of_rho_one,
   fun hρ => curvatureK_neg_substitute hJ hρ⟩

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:245

Module Section

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

In the same file