TensorCascadeDiagonalWard.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual enriched diagonal Ward residual, averaged over the cascade, retains the uniform bound proved for every fixed countable reference.

theorem OAI.InvariantIsing.expectedDiagonalWard_mixture_abs_le line 17

theorem OAI.InvariantIsing.tensorNamespaced_diagonal_principal_bound line 40

Source documentation

The diagonal spectral Ward bound for the actual finite tensor-enriched model, including all cascade, Haar and Gaussian averages.

theorem tensorNamespaced_diagonal_principal_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, (∑ a, (degree r a : ℝ)) ≤ D * ((r : ℝ) + 1))
    (b h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (J K : Finset (Fin N)) (hJK : Disjoint J K) :
    |tensorNamespacedReplicaAverage μ eig c I degree (tensorPerturbationAmplitude N u)
        n b treeDegree h (tensorDiagonalDirect eig J K (Prod.fst : Spin N × LabeledLeaf n → Spin N)) -
      tensorNamespacedReplicaAverage μ eig c I degree (tensorPerturbationAmplitude N u)
        n b treeDegree h (tensorDiagonalFresh eig J K (Prod.fst : Spin N × LabeledLeaf n → Spin N))| ≤
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorNamespacedReplicaAverage, OAI.InvariantIsing.tensorPerturbationAmplitude, OAI.InvariantIsing.tensorDiagonalDirect, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorDiagonalFresh