CavityPerturbationKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The overlap modulus of the finite Gaussian perturbation covariance. The geometric weights absorb the enumerated monomial degrees.

lemma OAI.InvariantIsing.cavity_monomial_difference line 15
lemma OAI.InvariantIsing.cavity_monomial_abs_le line 35

lemma OAI.InvariantIsing.cavity_spectral_tree_kernel_difference line 43

Source documentation

The common tree coordinate does not enlarge the overlap error.

lemma cavity_spectral_tree_kernel_difference {m : ℕ}
    (A B : Fin m → ℝ) (d : Fin m → ℕ) (r : ℕ) (q : ℝ)
    (hA : ∀ a, |A a| ≤ 1) (hB : ∀ a, |B a| ≤ 1) (hq : |q| ≤ 1)
    {δ : ℝ} (hd : ∀ a, |A a - B a| ≤ δ) :
    |(∏ a, A a ^ d a) * q ^ r - (∏ a, B a ^ d a) * q ^ r| ≤
      (∑ a, (d a : ℝ)) * δ := by
…

theorem OAI.InvariantIsing.cavity_weighted_covariance_difference line 58

Source documentation

Degree-weighted covariance errors are bounded independently of the number of perturbation monomials retained.

theorem cavity_weighted_covariance_difference {J m : ℕ}
    (A B : Fin m → ℝ) (degree : Fin J → Fin m → ℕ) (r : Fin J → ℕ) (q : ℝ)
    (hA : ∀ a, |A a| ≤ 1) (hB : ∀ a, |B a| ≤ 1) (hq : |q| ≤ 1)
    {δ D : ℝ} (hδ : 0 ≤ δ) (hd : ∀ a, |A a - B a| ≤ δ) (hD : 0 ≤ D)
    (hdegree : ∀ j, (∑ a, (degree j a : ℝ)) ≤ D * ((j : ℝ) + 1)) :
    |(∑ j : Fin J, perturbationWeight j ^ 2 * ((∏ a, A a ^ degree j a) * q ^ r j)) -
      ∑ j : Fin J, perturbationWeight j ^ 2 * ((∏ a, B a ^ degree j a) * q ^ r j)| ≤
      D * δ := by
…

theorem OAI.InvariantIsing.cavity_weighted_covariance_difference_amplitude line 84

Source documentation

The actual coefficient bound |u_j| ≤ 2 contributes a factor four.

theorem cavity_weighted_covariance_difference_amplitude {J m : ℕ}
    (A B : Fin m → ℝ) (degree : Fin J → Fin m → ℕ) (r : Fin J → ℕ) (q : ℝ)
    (u : Fin J → ℝ) (hu : ∀ j, |u j| ≤ 2)
    (hA : ∀ a, |A a| ≤ 1) (hB : ∀ a, |B a| ≤ 1) (hq : |q| ≤ 1)
    {δ D : ℝ} (hδ : 0 ≤ δ) (hd : ∀ a, |A a - B a| ≤ δ) (hD : 0 ≤ D)
    (hdegree : ∀ j, (∑ a, (degree j a : ℝ)) ≤ D * ((j : ℝ) + 1)) :
    |(∑ j : Fin J, perturbationWeight j ^ 2 * u j ^ 2 * ((∏ a, A a ^ degree j a) * q ^ r j)) -
      ∑ j : Fin J, perturbationWeight j ^ 2 * u j ^ 2 * ((∏ a, B a ^ degree j a) * q ^ r j)| ≤
      4 * D * δ := by
…