OAI/Probability/InvariantIsing/Arrays/NSpinTensorLabeled.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The finite spectral tensor model on the countable spin/leaf state space. The Gaussian energy marks are the actual pushforward of the coordinate marks, and the tilted ancestor-prefix marginal has its cascade value.

  1. def OAI.InvariantIsing.uniformSpinPrior line 19
  2. lemma OAI.InvariantIsing.finiteLogIntegral_uniformSpinPrior line 22
  3. lemma OAI.InvariantIsing.measurable_spinTensorEnergyMark line 33
  4. def OAI.InvariantIsing.tensorEnergyMarkLaw line 40
  5. lemma OAI.InvariantIsing.spinTensorEnergyMark_norm_le line 45
  6. lemma OAI.InvariantIsing.tensorEnergyMarkLaw_moments line 74
  7. def OAI.InvariantIsing.tensorSpinBaseEnergy line 96
  8. lemma OAI.InvariantIsing.tensorSpinBaseEnergy_add line 101
  9. theorem OAI.InvariantIsing.tensorCascadeValue_eq_energyRecursion line 112

    Source documentation

    Pushforward of the Gaussian energy marks commutes with the actual backward recursion. The terminal keeps the uniform probability Ising prior.

    theorem tensorCascadeValue_eq_energyRecursion {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 : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
    (z : SpinTensorIndex I degree → ℝ) :
    tensorCascadeValue eig U c I degree amplitude n b v z =
      IsingPerceptron.energyRecursion n b (fun i => tensorEnergyMarkLaw U I degree amplitude (v i))
        (uniformSpinPrior N : Measure (Spin N)) (tensorSpinBaseEnergy eig U c I degree amplitude z) := by
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeValue, OAI.IsingPerceptron.energyRecursion, OAI.InvariantIsing.tensorEnergyMarkLaw, OAI.InvariantIsing.uniformSpinPrior, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorSpinBaseEnergy

  10. abbrev OAI.InvariantIsing.TensorLabeledData line 146
  11. abbrev OAI.InvariantIsing.TensorLabeledState line 149
  12. def OAI.InvariantIsing.tensorLabeledLaw line 151
  13. abbrev OAI.InvariantIsing.TensorCoordinateData line 156
  14. def OAI.InvariantIsing.tensorCoordinateLaw line 160
  15. instance OAI.InvariantIsing.tensorCoordinateLaw_probability line 168
  16. def OAI.InvariantIsing.tensorEnergyCoordinates line 175
  17. lemma OAI.InvariantIsing.measurable_tensorEnergyCoordinates_joint line 180
  18. theorem OAI.InvariantIsing.tensorEnergyCoordinates_measurePreserving line 192
  19. instance OAI.InvariantIsing.tensorLabeledLaw_probability line 214
  20. def OAI.InvariantIsing.tensorLabeledReference line 221
  21. instance OAI.InvariantIsing.tensorLabeledReference_probability line 224
  22. lemma OAI.InvariantIsing.measurable_tensorLabeledReference line 229
  23. def OAI.InvariantIsing.tensorLabeledEnergy line 232
  24. lemma OAI.InvariantIsing.measurable_tensorLabeledEnergy line 237
  25. lemma OAI.InvariantIsing.measurable_tensorLabeledEnergy_root line 244
  26. theorem OAI.InvariantIsing.tensorLabeled_exp_integrable line 257
  27. theorem OAI.InvariantIsing.tensorLabeledLog_mean line 270
  28. theorem OAI.InvariantIsing.tensorLabeled_tilted_parent_tail line 289

    Source documentation

    The exact parent-prefix probability of two tilted replicas is the original cascade marginal, for the concrete tensor-enriched Ising model.

    theorem tensorLabeled_tilted_parent_tail {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 → ℝ) (d : Fin n) :
    (∫ p, IsingPerceptron.referenceReplicaMean (tensorLabeledReference N n p)
      (tensorLabeledEnergy eig U c I degree amplitude n z p)
      (fun σ : Fin 2 → TensorLabeledState N n =>
        if (IsingPerceptron.labeledAddress n (σ 1).2).take (d + 1) =
          (IsingPerceptron.labeledAddress n (σ 0).2).take (d + 1) then 1 else 0)
      ∂tensorLabeledLaw U I degree amplitude n b v) = 1 - b d :=
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.IsingPerceptron.CascadeExponents, OAI.IsingPerceptron.referenceReplicaMean, OAI.InvariantIsing.tensorLabeledReference, OAI.InvariantIsing.tensorLabeledEnergy, OAI.InvariantIsing.TensorLabeledState, OAI.IsingPerceptron.labeledAddress, OAI.InvariantIsing.tensorLabeledLaw