Documentation

Lean 4 Proof

theorem cesHessianQF_neg_semidef (hJ : 0 < J) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v) :
    cesHessianQF J ρ c v ≤ 0 := by
  rw [cesHessianQF_on_perp hJ ρ c hc v hv]
  apply mul_nonpos_of_nonpos_of_nonneg
  · simp only [cesEigenvaluePerp]
    apply div_nonpos_of_nonpos_of_nonneg
    · linarith
    · apply mul_nonneg
      · exact Nat.cast_nonneg J
      · linarith
  · simp only [vecNormSq]
    apply Finset.sum_nonneg
    intro j _
    exact sq_nonneg (v j)

Dependency Graph

Location

thesis/CESProofs/Foundations/Hessian.lean:81

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file