MagneticFieldHeightHessian.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual constrained finite-height Hessian. Differentiating the physical optimizing bias gives the scalar Schur-complement correction; no twice-differentiable optimizer is assumed.

lemma OAI.InvariantIsing.hasDerivAt_constrainedHeightFieldValue_line_at line 15
lemma OAI.InvariantIsing.hasDerivAt_magneticHeight_gradient line 41

lemma OAI.InvariantIsing.hasDerivAt_deriv_constrainedHeightFieldValue_line line 96

Source documentation

The second height derivative is the Hessian at the physical bias minus the rank-one correction from keeping the mean spin fixed.

lemma hasDerivAt_deriv_constrainedHeightFieldValue_line (h : FieldStep)
    {I : Set (Fin (h.depth + 1) → ℝ)} (F : FieldFiniteFamily (h.depth + 1) I)
    (hI : IsOpen I) (hU : F.U = fieldFiniteValue (fieldHeightFiniteList h))
    {s : ℝ} (hs : |s| < 1) (r d : Fin (h.depth + 1) → ℝ) (hr : r ∈ I)
    (hrs : r ∈ fieldStrictHeightCone h.depth) :
    HasDerivAt (deriv (fun t : ℝ => constrainedHeightFieldValue h s (r + t • d)))
      ((∑ i, ∑ j, F.PP i j (r, magneticHeightBias h s r) * d i * d j) -
        (∑ i, F.PX i (r, magneticHeightBias h s r) * d i) ^ 2 /
          F.XX (r, magneticHeightBias h s r)) 0 := by
…

Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.FieldFiniteFamily, OAI.InvariantIsing.fieldFiniteValue, OAI.InvariantIsing.fieldHeightFiniteList, OAI.InvariantIsing.fieldStrictHeightCone, OAI.InvariantIsing.constrainedHeightFieldValue, OAI.InvariantIsing.magneticHeightBias