OAI/Probability/InvariantIsing/Magnetic/MagneticFieldBias.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The physical mean spin is the bias derivative of the actual finite field functional, including its zero-exponent root Gaussian step.

  1. def OAI.InvariantIsing.fieldBiasMean line 16

    Source documentation

    The mean spin before the root increment, at an arbitrary bias.

    def fieldBiasMean (h : FieldStep) : ℝ → ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  2. lemma OAI.InvariantIsing.fieldValue_root line 21
  3. lemma OAI.InvariantIsing.fieldBiasMean_regular line 29
  4. lemma OAI.InvariantIsing.hasDerivAt_fieldValue_bias line 43
  5. lemma OAI.InvariantIsing.continuous_fieldValue_bias line 62