Documentation

Lean 4 Proof

theorem strategic_instability (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 1 < ρ)
    {c : ℝ} (hc : 0 < c)
    (δ : Fin J → ℝ) (hδ : orthToOne J δ) (hδ_ne : ∃ j, δ j ≠ 0) :
    0 < cesHessianQF J ρ c δ :=
  cesHessianQF_pos_on_perp hJ hρ hc δ hδ hδ_ne

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:179

Module Section

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

In the same file