CavityActualCovariance.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The cavity error bound for the actual finite Gaussian perturbation: the spectral/tree monomials, their amplitudes and dimension cutoff are kept explicit.

def OAI.InvariantIsing.cavityPerturbationCoefficients line 17
def OAI.InvariantIsing.cavityPerturbationKernel line 25
lemma OAI.InvariantIsing.cavityPerturbationCoefficients_cross line 30
lemma OAI.InvariantIsing.cavityPerturbationKernel_abs_le line 43
lemma OAI.InvariantIsing.cavityPerturbationCoefficients_sq_le line 54
lemma OAI.InvariantIsing.cavityPerturbationKernel_difference line 66

theorem OAI.InvariantIsing.cavity_actual_covariance_error line 87

Source documentation

The actual covariance error, including the additional monomials at dimension N+n, is controlled by the same vanishing rate.

theorem cavity_actual_covariance_error {N n m depth : ℕ}
    (U : Rotation (N + n)) (V : Rotation N)
    (I : Fin m → Finset (Fin (N + n))) (J : Fin m → Finset (Fin N))
    (u : ℕ → ℝ) (hu : ∀ j, |u j| ≤ 2)
    (σ₁ σ₂ : Spin (N + n)) (τ₁ τ₂ : Spin N) (α β : LabeledLeaf depth)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (herr : ∀ a, |projectedOverlap U (I a) σ₁ σ₂ - projectedOverlap V (J a) τ₁ τ₂| ≤ δ) :
    |cylinderCross (cavityPerturbationCoefficients U I u depth (σ₁, α))
        (cavityPerturbationCoefficients U I u depth (σ₂, β)) -
      cylinderCross (cavityPerturbationCoefficients V J u depth (τ₁, α))
        (cavityPerturbationCoefficients V J u depth (τ₂, β))| ≤
      4 * |(N + n) * perturbationScale (N + n) ^ 2 - N * perturbationScale N ^ 2| +
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.cavityPerturbationCoefficients