MagneticFieldHeightDerivative.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual height-direction envelope differentiation at fixed magnetization. The bias response is obtained by implicit differentiation of the finite physical mean, using its strictly positive curvature.

lemma OAI.InvariantIsing.hasFDerivAt_field_line_restriction line 15

lemma OAI.InvariantIsing.hasDerivAt_magneticHeightBias_line line 50

Source documentation

An arbitrary strict height direction has the explicitly differentiated physical optimizing bias.

lemma hasDerivAt_magneticHeightBias_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 (fun t : ℝ => magneticHeightBias h s (r + t • d))
      (-(∑ i, F.PX i (r, magneticHeightBias h s r) * d i) /
        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.magneticHeightBias

def OAI.InvariantIsing.constrainedHeightFieldValue line 73
Source documentation
The centered constrained field value on the strict height cone.
```
def constrainedHeightFieldValue (h : FieldStep) (s : ℝ)
    (r : Fin (h.depth + 1) → ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
lemma OAI.InvariantIsing.constrainedHeightFieldValue_eq line 78
lemma OAI.InvariantIsing.hasDerivAt_constrainedHeightFieldValue_line line 86