CavityIncrementComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite cavity increment after absorbing deterministic and Gaussian covariance errors. The base Gaussian field stays inside the Gibbs measure in the factor on the right.

lemma OAI.InvariantIsing.cavity_log_tilt_factor line 14
lemma OAI.InvariantIsing.cavity_mean_log_tilt_factor line 24

theorem OAI.InvariantIsing.cavity_log_increment_comparison line 54

Source documentation

The actual increment estimate used before passing to cavity limits. All error bounds concern the conditioned finite-size energies and covariances; no lower-bound conclusion is assumed.

theorem cavity_log_increment_comparison {X : Type*}
    [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X]
    (ν : Measure X) [IsProbabilityMeasure ν] (H W J V : X → ℝ) (c d : ℝ)
    {M L M₁ D B₀ B₁ : ℝ}
    (hH : ∀ x, |H x| ≤ M) (hW : ∀ x, |W x| ≤ L) (hJ : ∀ x, |J x| ≤ M₁)
    (hV : ∀ x, |V x| ≤ D) (hE : ∀ x, |J x - (H x + W x)| ≤ d * V x)
    (C A : X → ℕ →₀ ℝ)
    (hC : ∀ x, (C x).sum (fun _ z => z ^ 2) ≤ B₀)
    (hA : ∀ x, (A x).sum (fun _ z => z ^ 2) ≤ B₁)
    (hK : ∀ x y, |cylinderCross (A x) (A y) - cylinderCross (C x) (C y)| ≤
      c * (V x + V y)) :
    (∫ g : ℕ → ℝ, Real.log (∫ x, Real.exp (W x - (d + 2 * c) * V x)
…