OAI/Probability/InvariantIsing/Magnetic/MagneticFieldParameter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The bias infimum is finite and concave in the prescribed magnetization. Its actual minimizing bias supplies the supporting slope.

  1. lemma OAI.InvariantIsing.constrainedFieldValue_le_trial line 13
  2. lemma OAI.InvariantIsing.constrainedFieldValue_bounds line 17
  3. lemma OAI.InvariantIsing.concaveOn_constrainedFieldValue_magnetization line 29
  4. lemma OAI.InvariantIsing.constrainedFieldValue_bias_support line 46
  5. lemma OAI.InvariantIsing.constrainedFieldValue_magnetization_lipschitz line 57

    Source documentation

    An explicit local Lipschitz bound uniform over all field partitions whose total height is bounded.

    lemma constrainedFieldValue_magnetization_lipschitz (h : FieldStep)
    {s t r C : ℝ} (hr : r < 1) (hs : |s| ≤ r) (ht : |t| ≤ r)
    (hC : h.height (Fin.last h.depth) ≤ C) :
    |constrainedFieldValue h s - constrainedFieldValue h t| ≤
      ((Real.log 2 + C / 2) / (1 - r)) * |s - t| := by
…

    Mentions: OAI.InvariantIsing.FieldStep