Documentation

Lean 4 Proof

theorem cesHessianQF_pos_on_perp (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 1 < ρ)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v) (hv_ne : ∃ j, v j ≠ 0) :
    0 < cesHessianQF J ρ c v := by
  rw [cesHessianQF_on_perp (by omega) ρ c hc v hv]
  apply mul_pos (eigenvalue_perp_pos_substitute (by omega) hρ hc)
  obtain ⟨j₀, hj₀⟩ := hv_ne
  exact Finset.sum_pos' (fun j _ => sq_nonneg _) ⟨j₀, Finset.mem_univ _, by positivity⟩

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:82

Module Section

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

In the same file