Documentation

Lean 4 Proof

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

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Hessian.lean:101

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file