Documentation

Lean 4 Proof

theorem strategic_bound (hJ : 2 ≤ J) {ρ : ℝ} (_hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c)
    (δ : Fin J → ℝ) (hδ : orthToOne J δ) :
    cesHessianQF J ρ c δ =
      -(curvatureK J ρ / ((↑J - 1) * c)) * vecNormSq J δ := by
  -- From cesHessianQF_on_perp: cesHessianQF = -(1-ρ)/(Jc) * ||δ||^2
  -- And K/(J-1) = (1-ρ)(J-1)/(J(J-1)) = (1-ρ)/J
  -- So -K/((J-1)c) = -(1-ρ)/(Jc), and the two expressions are equal.
  rw [cesHessianQF_on_perp (by omega) ρ c hc δ hδ]
  simp only [cesEigenvaluePerp, curvatureK, vecNormSq]
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (by omega : 0 < J)
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  have hJm1_pos : (0 : ℝ) < ↑J - 1 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
    linarith
  have hJm1_ne : (↑J : ℝ) - 1 ≠ 0 := ne_of_gt hJm1_pos
  have hcne : c ≠ 0 := ne_of_gt hc
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:68

Module Section

Strategic independence of CES (Paper 1, Sections 7-8):

In the same file