PriorArrayDiagonalWard.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite diagonal Ward residual for the actual constrained-prior array.

lemma OAI.InvariantIsing.priorNamespacedArrayLaw_diagonalWard_residual line 13

theorem OAI.InvariantIsing.priorNamespacedArrayLaw_diagonalWard_bound line 52

Source documentation

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

theorem priorNamespacedArrayLaw_diagonalWard_bound {N m n : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
    (ν : Measure (Spin N × LabeledLeaf n)) [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, (∑ j, (degree r j : ℝ)) ≤ D * ((r : ℝ) + 1))
    (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
      (priorNamespacedArrayLaw μ ν eig c I degree (tensorPerturbationAmplitude N u) treeDegree h)
…

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