MagneticImplicitBias.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Parametric inversion of a strictly increasing physical mean spin. This supplies the finite-dimensional inverse-coordinate and envelope steps without assuming differentiability of the minimizing bias.

lemma OAI.InvariantIsing.parametric_bias_continuousAt line 16

lemma OAI.InvariantIsing.parametric_bias_hasDerivAt line 41

Source documentation

The implicit bias derivative follows from the derivative of the actual mean-spin map and the local root equation.

lemma parametric_bias_hasDerivAt {A : ℝ × ℝ → ℝ} {b : ℝ → ℝ} {t s a c : ℝ}
    (hb : ContinuousAt b t) (hc : c ≠ 0)
    (hA : HasFDerivAt A (pairLinear a c) (t, b t))
    (he : ∀ᶠ q in 𝓝 t, A (q, b q) = s) :
    HasDerivAt b (-a / c) t := by
…

lemma OAI.InvariantIsing.parametric_bias_envelope line 74

Source documentation

Envelope differentiation with the bias response derived, rather than postulated, from the physical mean-spin equation.

lemma parametric_bias_envelope {U A : ℝ × ℝ → ℝ} {b : ℝ → ℝ}
    {t s a c v : ℝ} (hb : ContinuousAt b t) (hc : c ≠ 0)
    (hA : HasFDerivAt A (pairLinear a c) (t, b t))
    (he : ∀ᶠ q in 𝓝 t, A (q, b q) = s)
    (hU : HasFDerivAt U (pairLinear v s) (t, b t)) :
    HasDerivAt (fun q => U (q, b q) - b q * s) v t := by
…