Documentation

Lean 4 Proof

theorem cesHessianQF_on_one (_hJ : 0 < J) (ρ c : ℝ) (_hc : 0 < c) (α : ℝ) :
    cesHessianQF J ρ c (fun _ => α) = 0 := by
  simp only [cesHessianQF]
  rw [Finset.sum_const, Finset.sum_const, Finset.card_univ, Fintype.card_fin]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/Hessian.lean:61

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file