Documentation

Lean 4 Proof

theorem manipulation_magnitude (hJ : 2 ≤ J) (ρ : ℝ)
    {c : ℝ} (hc : 0 < c)
    (δ : Fin J → ℝ) (hδ : orthToOne J δ) :
    |cesHessianQF J ρ c δ| =
      |curvatureK J ρ| / ((↑J - 1) * c) * vecNormSq J δ := by
  rw [hessianQF_eq_negK_norm hJ ρ hc δ hδ]
  have hJ1 : (0 : ℝ) < ↑J - 1 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith
  have hvn : 0 ≤ vecNormSq J δ := by
    simp only [vecNormSq]; exact Finset.sum_nonneg (fun j _ => sq_nonneg _)
  rw [abs_mul, abs_neg, abs_div, abs_of_pos (mul_pos hJ1 hc), abs_of_nonneg hvn]

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:257

Module Section

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

In the same file