OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.priorSpectralGGResidual line 14
2. lemma OAI.InvariantIsing.measurable_ggFresh line 29

   Also declared: OAI/Probability/InvariantIsing/Arrays/TensorFiniteGG.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/Arrays/TensorFiniteGG.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/Arrays/TensorFiniteGG.lean:54 (same declaration text), OAI/Probability/InvariantIsing/Fields/SpinPriorFiniteGG.lean:54 (same declaration text).

5. theorem OAI.InvariantIsing.priorFiniteGG_bound line 69
6. theorem OAI.InvariantIsing.priorFiniteGG_individualDiagonal_bound line 146

   Source documentation

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

   theorem priorFiniteGG_individualDiagonal_bound {N m k n q : ℕ}
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
       (ν₀ : Measure (Spin N × LabeledLeaf n)) [IsProbabilityMeasure ν₀] (eig c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (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, priorNamespacedObservableAverage μ ν₀ eig c I degree amplitude r h
         (fun U x => |projectedOverlap (specialRotation U) (I a) x.1 x.1 - center a|) ≤ δ a)
       (hE :
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.priorNamespacedObservableAverage, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.specialRotation