OAI/Probability/InvariantIsing/Arrays/TensorFiniteGG.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorSpectralGGResidual line 15
2. lemma OAI.InvariantIsing.measurable_ggFresh line 29

   Also declared: OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean:29 (same declaration text), OAI/Probability/InvariantIsing/Fields/SpinPriorFiniteGG.lean:29 (same declaration text).

3. lemma OAI.InvariantIsing.measurable_ggPair line 44

   Also declared: OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean:44 (same declaration text), OAI/Probability/InvariantIsing/Fields/SpinPriorFiniteGG.lean:44 (same declaration text).

4. lemma OAI.InvariantIsing.measurable_ggOld line 54

   Also declared: OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean:54 (same declaration text), OAI/Probability/InvariantIsing/Fields/SpinPriorFiniteGG.lean:54 (same declaration text).

5. theorem OAI.InvariantIsing.tensorFiniteGG_bound line 69
6. theorem OAI.InvariantIsing.tensorFiniteGG_individualDiagonal_bound line 145

   Source documentation

   Each individual self-overlap error controls every selected tensor covariance. The Gaussian energy error is expressed in the same actual model.

   theorem tensorFiniteGG_individualDiagonal_bound {N m k q : ℕ}
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (b : ℕ → ℝ) (r : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
       (j : Fin k) (β e C : ℝ) (hC : 0 ≤ C) (ha : 0 < |amplitude j|)
       (D : SpecialOrthogonal N → (Fin (q + 1) → Spin N × LabeledLeaf n) → ℝ)
       (hD : Measurable (Function.uncurry D)) (hDb : ∀ U σ, |D U σ| ≤ C)
       (center δ : Fin m → ℝ)
       (hδ : ∀ a, tensorNamespacedObservableAverage μ eig c I degree amplitude n b r h
         (fun U x => |projectedOverlap (specialRotation U) (I a) x.1 x.1 - center a|) ≤ δ a)
       (hE :
         let A := spectralPerturbationCoefficients (fun ω : TensorFrozenData N n j => ω.1.1)
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorNamespacedObservableAverage, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.spectralPerturbationCoefficients, OAI.InvariantIsing.TensorFrozenData