OAI/Probability/InvariantIsing/Arrays/NSpinTensorCascade.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The finite spectral-monomial enriched Ising model. Gaussian marks have a separate variance at every site/tensor coordinate and every cascade level. The spectral coefficients retain their actual dependence on the rotation.

  1. abbrev OAI.InvariantIsing.SpinTensorIndex line 19
  2. def OAI.InvariantIsing.spinTensorFeature line 23
  3. lemma OAI.InvariantIsing.measurable_spinTensorFeature line 29
  4. def OAI.InvariantIsing.tensorVarianceProfile line 39

    Source documentation

    Variances shared by the coordinates of each spectral monomial.

    def tensorVarianceProfile {N m k : ℕ} (I : Fin m → Finset (Fin N))
    (degree : Fin k → Fin m → ℕ) (site : ℝ≥0) (monomial : Fin k → ℝ≥0) :
    SpinTensorIndex I degree → ℝ≥0
  | Sum.inl _ => site
  | Sum.inr v => monomial v.1

/-- The concrete Gaussian covariance is the linear spin-field kernel plus
the required finite sum of spectral-overlap monomials. -/

    Mentions: OAI.InvariantIsing.SpinTensorIndex

  5. theorem OAI.InvariantIsing.spinTensorFeature_covariance line 47

    Source documentation

    The concrete Gaussian covariance is the linear spin-field kernel plus the required finite sum of spectral-overlap monomials.

    theorem spinTensorFeature_covariance {N m k : ℕ} (U : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (site : ℝ≥0) (monomial : Fin k → ℝ≥0) (σ τ : Spin N) :
    (∑ i : SpinTensorIndex I degree, (tensorVarianceProfile I degree site monomial i : ℝ) *
      spinTensorFeature U I degree amplitude σ i * spinTensorFeature U I degree amplitude τ i) =
      (site : ℝ) * (∑ i, spinValue (σ i) * spinValue (τ i)) +
        ∑ j, (monomial j : ℝ) * amplitude j ^ 2 *
          ∏ a, projectedOverlap U (I a) σ τ ^ degree j a := by
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorVarianceProfile, OAI.InvariantIsing.spinTensorFeature, OAI.InvariantIsing.spinValue, OAI.InvariantIsing.projectedOverlap

  6. theorem OAI.InvariantIsing.spinTensorFeature_variance_le line 75
  7. def OAI.InvariantIsing.spinTensorEnergy line 99
  8. def OAI.InvariantIsing.spinTensorTerminal line 104
  9. lemma OAI.InvariantIsing.measurable_spinTensorTerminal line 110
  10. lemma OAI.InvariantIsing.measurable_spinTensorTerminal_joint line 117
  11. lemma OAI.InvariantIsing.spinTensorTerminal_linearGrowth line 136
  12. def OAI.InvariantIsing.tensorGaussianLaw line 173
  13. lemma OAI.InvariantIsing.tensorGaussianLaw_moments line 178
  14. def OAI.InvariantIsing.tensorCascadeLaw line 193
  15. def OAI.InvariantIsing.tensorCascadeLog line 200
  16. def OAI.InvariantIsing.tensorCascadeValue line 208
  17. def OAI.InvariantIsing.tensorLeafState line 216

    Source documentation

    The actual sum of the root and all Gaussian marks on a sampled leaf.

    def tensorLeafState {N m k : ℕ} (I : Fin m → Finset (Fin N))
    (degree : Fin k → Fin m → ℕ) : (n : ℕ) → (SpinTensorIndex I degree → ℝ) →
    IsingPerceptron.NoiseLeaf (SpinTensorIndex I degree → ℝ) n → (SpinTensorIndex I degree → ℝ)
  | 0, z, _ => z
  | n + 1, z, leaf => tensorLeafState I degree n (z + leaf.2.1) leaf.2.2

    Mentions: OAI.InvariantIsing.SpinTensorIndex, OAI.IsingPerceptron.NoiseLeaf

  18. lemma OAI.InvariantIsing.noiseLeafTerminal_spinTensorTerminal line 222
  19. theorem OAI.InvariantIsing.tensorCascadeLog_eq_jointPartition line 236

    Source documentation

    The cascade logarithm is the actual spin/leaf joint partition, with uniform Ising prior and the sampled cascade leaf law.

    theorem tensorCascadeLog_eq_jointPartition {N m k : ℕ}
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (z : SpinTensorIndex I degree → ℝ)
    (T : IsingPerceptron.NoiseTree (SpinTensorIndex I degree → ℝ) n) :
    tensorCascadeLog eig U c I degree amplitude n z T =
      Real.log (∫ leaf, (Fintype.card (Spin N) : ℝ)⁻¹ * ∑ σ : Spin N,
        Real.exp (rotatedEnergy eig U σ + fieldEnergy c σ +
          spinTensorEnergy U I degree amplitude (tensorLeafState I degree n z leaf) σ)
        ∂IsingPerceptron.noiseLeafKernel (SpinTensorIndex I degree → ℝ) n T) := by
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.IsingPerceptron.NoiseTree, OAI.InvariantIsing.tensorCascadeLog, OAI.InvariantIsing.Spin, OAI.InvariantIsing.rotatedEnergy, OAI.InvariantIsing.fieldEnergy, OAI.InvariantIsing.spinTensorEnergy, OAI.InvariantIsing.tensorLeafState, OAI.IsingPerceptron.noiseLeafKernel

  20. theorem OAI.InvariantIsing.tensorCascadeLog_recursion line 259

    Source documentation

    Exact leaf-law recursion and conditional centered fluctuation for the finite spectral tensor perturbations. The Haar rotation is retained in every coefficient; the statement holds separately for every rotation.

    theorem tensorCascadeLog_recursion {N m k : ℕ} (hN : 0 < N)
    (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (hb : IsingPerceptron.CascadeExponents n b) (z : SpinTensorIndex I degree → ℝ) :
    let P := tensorCascadeLaw I degree n b v
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.tensorCascadeLaw

  21. lemma OAI.InvariantIsing.measurable_tensorCascadeValue_joint line 292
  22. lemma OAI.InvariantIsing.integrable_tensorCascadeValue_root line 307
  23. def OAI.InvariantIsing.tensorEnrichedPressure line 332
  24. theorem OAI.InvariantIsing.tensorEnrichedPressure_eq_cascade_expectation line 339