OAI/Probability/InvariantIsing/Fields/FieldCascade.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite one-site functional as a Gaussian cascade expectation.

  1. def OAI.InvariantIsing.fieldCascadeVariance line 14
  2. def OAI.InvariantIsing.fieldCascadeLaw line 18
  3. lemma OAI.InvariantIsing.fieldCascadeFold_eq_magneticRecursion line 21
  4. theorem OAI.InvariantIsing.fieldCascadeLog_recursion line 36
  5. theorem OAI.InvariantIsing.fieldValue_eq_cascade_expectation line 51

    Source documentation

    The finite one-site entropy value equals the root Gaussian average of the logarithm of the Gaussian-marked cascade integral, with its prescribed diagonal covariance subtraction.

    theorem fieldValue_eq_cascade_expectation (h : FieldStep) :
    fieldValue h 0 =
      (∫ g, (∫ T, gaussianCascadeLog h.depth (Real.sqrt (h.height 0) * g) T
        ∂fieldCascadeLaw h) ∂gaussianReal 0 1) - h.height (Fin.last h.depth) / 2 := by
…

    Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.InvariantIsing.gaussianCascadeLog, OAI.InvariantIsing.fieldCascadeLaw