OAI/Probability/InvariantIsing/Arrays/NSpinCascade.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Gaussian cascade marking for the actual finite Ising partition function at a fixed orthogonal rotation. The Haar variable is fixed in this result.

  1. def OAI.InvariantIsing.rotatedFieldTerminal line 19
  2. lemma OAI.InvariantIsing.measurable_rotatedFieldTerminal line 23
  3. lemma OAI.InvariantIsing.abs_rotatedFieldTerminal_sub_le line 28
  4. lemma OAI.InvariantIsing.rotatedFieldTerminal_linearGrowth line 44
  5. def OAI.InvariantIsing.vectorGaussianLaw line 54
  6. lemma OAI.InvariantIsing.vectorGaussianLaw_moments line 57
  7. def OAI.InvariantIsing.rotatedCascadeLaw line 69
  8. def OAI.InvariantIsing.rotatedCascadeLog line 73
  9. def OAI.InvariantIsing.rotatedCascadeValue line 79
  10. theorem OAI.InvariantIsing.rotatedCascadeLog_recursion line 86

    Source documentation

    The published Gaussian marking recursion specialized to the actual finite rotated Ising terminal, with the Haar rotation held fixed.

    theorem rotatedCascadeLog_recursion {N : ℕ} (hN : 0 < N) (n : ℕ) (b : ℕ → ℝ)
    (v : ℕ → ℝ≥0) (hb : IsingPerceptron.CascadeExponents n b)
    (eig : Fin N → ℝ) (U : Rotation N) (c z : Fin N → ℝ) :
    Integrable (rotatedCascadeLog n eig U c z) (rotatedCascadeLaw N n b v) ∧
      (∫ T, rotatedCascadeLog n eig U c z T ∂rotatedCascadeLaw N n b v) =
        rotatedCascadeValue n b v eig U c z := by
…

    Mentions: OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.rotatedCascadeLog, OAI.InvariantIsing.rotatedCascadeLaw, OAI.InvariantIsing.rotatedCascadeValue

  11. lemma OAI.InvariantIsing.integrable_rotatedCascadeValue line 101
  12. def OAI.InvariantIsing.rotatedEnrichedPressure line 124
  13. theorem OAI.InvariantIsing.rotatedEnrichedPressure_eq_cascade_expectation line 131

    Source documentation

    The fixed-rotation enriched pressure is the actual iterated Gaussian root and cascade expectation of the finite Ising log partition.

    theorem rotatedEnrichedPressure_eq_cascade_expectation {N : ℕ} (hN : 0 < N)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → ℝ≥0) (root : ℝ≥0)
    (hb : IsingPerceptron.CascadeExponents n b)
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ) :
    rotatedEnrichedPressure n b v root eig U c =
      (N : ℝ)⁻¹ * ∫ z, (∫ T, rotatedCascadeLog n eig U c z T
        ∂rotatedCascadeLaw N n b v) ∂(vectorGaussianLaw N root : Measure (Fin N → ℝ)) := by
…

    Mentions: OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.rotatedEnrichedPressure, OAI.InvariantIsing.rotatedCascadeLog, OAI.InvariantIsing.rotatedCascadeLaw, OAI.InvariantIsing.vectorGaussianLaw