Documentation

Lean 4 Proof

theorem saddle_point_substitutes
    (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 1 < ρ)
    {c : ℝ} (hc : 0 < c)
    (v : Fin J → ℝ) (hv : orthToOne J v)
    (hv_ne : ∃ j, v j ≠ 0) :
    0 < cesHessianQF J ρ c v := by
  rw [cesHessianQF_on_perp (by omega) ρ c hc v hv]
  apply mul_pos
  · simp only [cesEigenvaluePerp]
    apply div_pos (by linarith)
    exact mul_pos (by exact_mod_cast (by omega : 0 < J)) hc
  · exact Finset.sum_pos'
      (fun j _ => sq_nonneg (v j))
      (by obtain ⟨j₀, hj₀⟩ := hv_ne
          exact ⟨j₀, Finset.mem_univ _, by positivity⟩)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:74

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file