Documentation

Lean 4 Proof

theorem eigenvalue_perp_pos_substitute (hJ : 0 < J) {ρ : ℝ} (hρ : 1 < ρ)
    {c : ℝ} (hc : 0 < c) :
    0 < cesEigenvaluePerp J ρ c := by
  simp only [cesEigenvaluePerp]
  exact div_pos (neg_pos.mpr (by linarith)) (mul_pos (Nat.cast_pos.mpr hJ) hc)

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:62

Module Section

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

In the same file