Documentation

Lean 4 Proof

theorem hessianQF_eq_negK_norm (hJ : 2 ≤ J) (ρ : ℝ)
    {c : ℝ} (hc : 0 < c)
    (δ : Fin J → ℝ) (hδ : orthToOne J δ) :
    cesHessianQF J ρ c δ =
      -(curvatureK J ρ / ((↑J - 1) * c)) * vecNormSq J δ := by
  rw [cesHessianQF_on_perp (by omega) ρ c hc δ hδ]
  simp only [cesEigenvaluePerp, curvatureK, vecNormSq]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hJm1_ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith
  have hcne : c ≠ 0 := ne_of_gt hc
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:157

Module Section

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

In the same file