OAI/Probability/InvariantIsing/Magnetic/MagneticFieldFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Identification of the joint finite-height derivatives with the actual physical mean and curvature at every bias.

  1. lemma OAI.InvariantIsing.fieldFiniteFamily_mean_at_bias line 15
  2. lemma OAI.InvariantIsing.fieldFiniteFamily_curvature_at_bias line 30
  3. lemma OAI.InvariantIsing.fieldFiniteFamily_curvature_pos line 43
  4. def OAI.InvariantIsing.magneticHeightBias line 52

    Source documentation

    The unique interior minimizing bias for the actual literal height vector.

    def magneticHeightBias (h : FieldStep) (s : ℝ) (r : Fin (h.depth + 1) → ℝ) : ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  5. lemma OAI.InvariantIsing.magneticHeightBias_eq line 56
  6. lemma OAI.InvariantIsing.fieldFiniteFamily_magneticHeightBias line 61
  7. lemma OAI.InvariantIsing.continuousAt_magneticHeightBias_line line 70