OAI/Probability/InvariantIsing/Cavity/CavityFiniteIncrement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.cavityJoinedSpin line 15
2. theorem OAI.InvariantIsing.cavity_finite_energy_increment line 21

   Source documentation

   Conditional on the coupled spectral geometry, the actual finite perturbations cost a vanishing coefficient times the special-coordinate penalty. The Gaussian perturbation stays inside the base Gibbs law.

   theorem cavity_finite_energy_increment {N n m depth : ℕ} (hN : 0 < N)
       (U : Rotation (N + n)) (V : Rotation N)
       (I : Fin m → Finset (Fin (N + n))) (J : Fin m → Finset (Fin N))
       (eig : Fin (N + n) → ℝ) (eig₀ : Fin N → ℝ)
       (v : Fin m → ℝ) (hv : ∀ a, |v a| ≤ 2)
       (u : ℕ → ℝ) (hu : ∀ j, |u j| ≤ 2) (t : ℝ)
       (ν : Measure ((Spin N × Spin n) × LabeledLeaf depth)) [IsProbabilityMeasure ν]
       (w : Spin N × Spin n → ℝ) (hw : ∀ x, 1 ≤ w x)
       {C : ℝ} (hC : 0 ≤ C)
       (herr : ∀ x y a, |projectedOverlap U (I a) (cavityJoinedSpin x) (cavityJoinedSpin y) -
         projectedOverlap V (J a) x.1 y.1| ≤ C / N * (w x + w y)) :
       let H := fun x : (Spin N × Spin n) × LabeledLeaf depth =>
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.cavityJoinedSpin