Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Potential/Appendix.lean:41

Module Section

Appendix Lemmas 1-3 (Paper 2, Appendix A)

In the same file