OAI/Probability/InvariantIsing/Arrays/TensorArrayDiagonalWard.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.spectralDiagonalWardDirect line 17
2. def OAI.InvariantIsing.spectralDiagonalWardFresh line 22
3. lemma OAI.InvariantIsing.continuous_spectralDiagonalWardDirect line 26
4. lemma OAI.InvariantIsing.continuous_spectralDiagonalWardFresh line 31
5. lemma OAI.InvariantIsing.spectralDiagonalWardResidual_integral line 36
6. lemma OAI.InvariantIsing.tensorNamespacedArrayLaw_diagonalWard_residual line 58
7. theorem OAI.InvariantIsing.tensorNamespacedArrayLaw_diagonalWard_bound line 96

   Source documentation

   Exact finite-volume spectral-array diagonal Ward bound for the actual tensor-enriched law, before taking any overlap limit.

   theorem tensorNamespacedArrayLaw_diagonalWard_bound {N m n : ℕ} (hN : 0 < N)
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
       (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, (∑ j, (degree r j : ℝ)) ≤ D * ((r : ℝ) + 1))
       (b h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
       (κ : Fin m → ℝ) (a d : Fin m) (had : Disjoint (I a) (I d))
       (ha : ∀ i ∈ I a, eig i = κ a) (hd : ∀ i ∈ I d, eig i = κ d) :
       |spectralDiagonalWardResidual
         (tensorNamespacedArrayLaw μ eig c I degree (tensorPerturbationAmplitude N u) n b treeDegree h)
         (fun j => ((I j).card : ℝ) / N) κ a d| ≤ 48 * D * perturbationScale N ^ 2 := by
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.spectralDiagonalWardResidual, OAI.InvariantIsing.tensorNamespacedArrayLaw, OAI.InvariantIsing.tensorPerturbationAmplitude