OAI/Probability/InvariantIsing/Fields/FieldBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the one-site entropy

The finite Gaussian recursion agrees with the Ising recursion. In particular the zero overlap path has entropy zero. This supplies the exact variational normalization for a point-mass spectral law.

  1. lemma OAI.InvariantIsing.gaussianOperator_eq_transform line 21
  2. def OAI.InvariantIsing.heightSequence line 28

    Source documentation

    Extend the last covariance height constantly.

    def heightSequence (h : FieldStep) (i : ℕ) : ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  3. lemma OAI.InvariantIsing.heightSequence_mono line 31
  4. lemma OAI.InvariantIsing.heightSequence_nonneg line 36
  5. lemma OAI.InvariantIsing.heightSequence_eq line 39
  6. lemma OAI.InvariantIsing.fieldValue_eq_magneticFieldValue line 45

    Source documentation

    Equality with the scalar recursion, including its root Gaussian average and diagonal covariance subtraction.

    lemma fieldValue_eq_magneticFieldValue (h : FieldStep) :
    fieldValue h 0 = IsingPerceptron.magneticFieldValue h.depth
      (IsingPerceptron.chainExponent h.cut) (heightSequence h) := by
…

    Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.IsingPerceptron.magneticFieldValue, OAI.IsingPerceptron.chainExponent, OAI.InvariantIsing.heightSequence

  7. lemma OAI.InvariantIsing.fieldValue_nonpos line 93
  8. lemma OAI.InvariantIsing.entropyFunctional_zero line 99
  9. lemma OAI.InvariantIsing.variationalFunctional_constant line 108