FieldFiniteSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite height Hessian criterion and its supporting-plane consequence. The conclusion assumes the mixed and radial derivative signs of the scalar Ising recursion.

lemma OAI.InvariantIsing.FieldFiniteFamily.hessian_nonpos line 19

theorem OAI.InvariantIsing.FieldFiniteFamily.support_of_hessian line 34

Source documentation

A supporting plane follows from the Hessian sign criterion along a segment. Existence of the second derivatives suffices; continuity of the second derivatives is not assumed.

theorem support_of_hessian (hI : Convex ℝ I) (r s : Fin n → ℝ) (z : ℝ)
    (hr : r ∈ I) (hs : s ∈ I)
    (hq : ∀ t ∈ Icc (0 : ℝ) 1,
      ∑ i, ∑ j, F.PP i j (r + t • (s - r), z) * (s i - r i) * (s j - r j) ≤ 0) :
    F.U (s, z) ≤ F.U (r, z) + ∑ i, F.P i (r, z) * (s i - r i) := by
…