OAI/Probability/InvariantIsing/Arrays/TensorTruncatedWard.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The finite spin/leaf pair application of the spectral Haar Ward identity. The spin test is fixed under rotations and may be any function of total overlap. Arbitrary finite leaf restrictions and zero prior weights are allowed.

  1. def OAI.InvariantIsing.tensorRestrictionBase line 18
  2. def OAI.InvariantIsing.tensorRestrictionOffObservable line 22
  3. def OAI.InvariantIsing.tensorRestrictionOffVariation line 27
  4. def OAI.InvariantIsing.tensorRestrictionMainVariation line 32
  5. def OAI.InvariantIsing.tensorRestrictionPairPrefix line 37
  6. def OAI.InvariantIsing.tensorRestrictionPairPlanePrefix line 44
  7. def OAI.InvariantIsing.tensorRestrictionPairBase line 51
  8. theorem OAI.InvariantIsing.tensorRestriction_off_ward_prefix line 57

    Source documentation

    Exact Haar/Gaussian Ward equation for the actual finite tensor model on any finite spin/leaf restriction, with a finite Gaussian prefix.

    theorem tensorRestriction_off_ward_prefix [Fintype S] {N m k n d : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    {w : S → ℝ} (hw : GibbsReference w) (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0) (x : S → Spin N × LabeledLeaf n)
    (i j : Fin N) (hij : i ≠ j) (F : Spin N → Spin N → ℝ)
    (B : ℝ) (hB : 0 ≤ B) (hF : ∀ σ τ, |F σ τ| ≤ B) :
    let wp := fun p : S × S => w p.1 * w p.2
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin

  9. def OAI.InvariantIsing.tensorRestrictionPairHamiltonian line 177
  10. def OAI.InvariantIsing.tensorRestrictionPairCovarianceDerivative line 185
  11. lemma OAI.InvariantIsing.measurable_gaussianWardCorrection line 195
  12. theorem OAI.InvariantIsing.tensorRestriction_off_ward line 215

    Source documentation

    The actual finite spin/leaf pair Ward equation, using the complete Gaussian coordinate law.

    theorem tensorRestriction_off_ward [Fintype S] {N m k n : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    {w : S → ℝ} (hw : GibbsReference w) (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0) (x : S → Spin N × LabeledLeaf n)
    (i j : Fin N) (hij : i ≠ j) (F : Spin N → Spin N → ℝ)
    (B : ℝ) (hB : 0 ≤ B) (hF : ∀ σ τ, |F σ τ| ≤ B) :
    let wp := fun p : S × S => w p.1 * w p.2
…

    Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin