OAI/Probability/InvariantIsing/Arrays/TensorDiagonalPrincipalWard.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.expectedDiagonalWard line 17
2. theorem OAI.InvariantIsing.expectedDiagonalWard_restriction_tendsto line 23
3. theorem OAI.InvariantIsing.expectedDiagonalWard_abs_le_of_restriction line 39
4. lemma OAI.InvariantIsing.expectedDiagonalWard_subtype line 56
5. lemma OAI.InvariantIsing.tensorRestrictionDiagonalVariation_principal_eq line 81
6. lemma OAI.InvariantIsing.tensorRestriction_diagonal_integral_pair line 115
7. lemma OAI.InvariantIsing.tensorRestrictionDiagonalVariation_principal_integral line 136
8. theorem OAI.InvariantIsing.tensorRestriction_diagonal_principal_bound line 178

   Source documentation

   The actual finite diagonal Ward residual has a uniform quadratic perturbation bound, with no limiting Ward assumption.

   theorem tensorRestriction_diagonal_principal_bound {N m n : ℕ} (hN : 0 < N)
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
       (ν : Measure S) [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, (∑ a, (degree r a : ℝ)) ≤ D * ((r : ℝ) + 1))
       (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0) (x : S → Spin N × LabeledLeaf n)
       (J K : Finset (Fin N)) (hJK : Disjoint J K) :
       let amp := tensorPerturbationAmplitude N u
   …

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