Documentation

Lean 4 Proof

theorem cesHessianQF_pos_semidef_substitute (hJ : 0 < J) {ρ : ℝ} (hρ : 1 < ρ)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v) :
    0 ≤ cesHessianQF J ρ c v := by
  rw [cesHessianQF_on_perp hJ ρ c hc v hv]
  exact mul_nonneg (le_of_lt (eigenvalue_perp_pos_substitute hJ hρ hc))
    (Finset.sum_nonneg (fun j _ => sq_nonneg (v j)))

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:71

Module Section

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

In the same file