OAI/Probability/InvariantIsing/Arrays/TensorPrincipalWard.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.referenceReplicaMean_finite_finset_sum line 19
2. lemma OAI.InvariantIsing.finiteGibbsVariation_pair_scaled_reference line 26
3. lemma OAI.InvariantIsing.tensorRestrictionOffVariation_principal_eq line 42
4. lemma OAI.InvariantIsing.integral_normalized_double_sum line 90
5. lemma OAI.InvariantIsing.normalized_integral_sum_eq_neg line 102
6. def OAI.InvariantIsing.tensorRestrictionOffPrincipalVariation line 120
7. lemma OAI.InvariantIsing.tensorRestriction_off_integral_pair line 130
8. lemma OAI.InvariantIsing.integrable_finite_referenceReplicaMean line 155
9. lemma OAI.InvariantIsing.tensorRestrictionOffVariation_principal_integral line 164
10. theorem OAI.InvariantIsing.tensorRestriction_off_principal_bound line 211

    Source documentation

    For the actual finite-prior tensor model, the principal Ward residual is bounded by the Gaussian correction. The direct and fresh observables use the original state prior and a generic spin projection, so they survive countable leaf restriction unchanged.

    theorem tensorRestriction_off_principal_bound {N m n : ℕ} (hN : 0 < N)
        (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
        (ν : Measure S) [IsProbabilityMeasure ν] (eig c : Fin N → ℝ)
        (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ) (treeDegree : Fin N → ℕ)
        (u : Fin N → ℝ) (hu : ∀ r, |u r| ≤ 2) (D : ℝ) (hD : 0 ≤ D)
        (hdegree : ∀ r, (∑ a, (degree r a : ℝ)) ≤ D * ((r : ℝ) + 1))
        (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0) (x : S → Spin N × LabeledLeaf n)
        (J K : Finset (Fin N)) (hJK : Disjoint J K)
        (F : Spin N → Spin N → ℝ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ σ τ, |F σ τ| ≤ B) :
        let amp := tensorPerturbationAmplitude N u
    …

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