CavityFiniteCappedIncrement.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The capped finite increment for the actual Ising energies and tensor perturbations, retaining the full base Gaussian Gibbs measure.

theorem OAI.InvariantIsing.cavity_finite_capped_energy_increment line 18

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_capped_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 cap : ℝ) (hcap : 0 ≤ cap)
    (ν : 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