OAI/Probability/InvariantIsing/Magnetic/MagneticInverseVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Local inverse-mean-coordinate calculus used by the prescribed-spin field comparison. These identities derive the change of curvature and the second derivative of a pulled-back field variation.

  1. lemma OAI.InvariantIsing.inverse_mean_curvature_variation line 15
  2. lemma OAI.InvariantIsing.inverse_mean_pullback_derivative line 27
  3. lemma OAI.InvariantIsing.inverse_mean_pullback_quotient line 35

    Source documentation

    The spatial derivative of the first inverse-coordinate derivative. This is the local formula behind delta a = a^2 delta F_uu.

    lemma inverse_mean_pullback_quotient {Z V₁ C : ℝ → ℝ} {u c v v₂ d : ℝ}
    (hc : c ≠ 0) (hZ : HasDerivAt Z (1 / c) u)
    (hv : V₁ (Z u) = v) (hcv : C (Z u) = c)
    (hV : HasDerivAt V₁ v₂ (Z u)) (hC : HasDerivAt C d (Z u)) :
    HasDerivAt (fun q => V₁ (Z q) / C (Z q))
      (v₂ / c ^ 2 - v * d / c ^ 3) u := by
…
  4. lemma OAI.InvariantIsing.inverse_mean_pullback_second line 48
  5. lemma OAI.InvariantIsing.inverse_mean_variation_identity line 60