Documentation

Lean 4 Proof

theorem cesHessianQF_on_perp (hJ : 0 < J) (ρ c : ℝ) (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v) :
    cesHessianQF J ρ c v = cesEigenvaluePerp J ρ c * vecNormSq J v := by
  simp only [cesHessianQF, cesEigenvaluePerp, orthToOne, vecSum, vecNormSq] at *
  rw [hv]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hcne : c ≠ 0 := ne_of_gt hc
  field_simp
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Hessian.lean:69

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file