CountableWardFunctional.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded two- and three-replica Ward terms pass through leaf exhaustion. A finite Ward bound is preserved in the countable-leaf limit.

def OAI.InvariantIsing.expectedReplicaWard line 15
theorem OAI.InvariantIsing.expectedReplicaWard_restriction_tendsto line 21

theorem OAI.InvariantIsing.expectedReplicaWard_abs_le_of_restriction line 41

Source documentation

Uniform finite Ward residual bounds are preserved for the full countable Gibbs prior. No convergence or integrability of a Gaussian correction is needed.

theorem expectedReplicaWard_abs_le_of_restriction {Ω X : Type*}
    [MeasurableSpace Ω] [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X]
    (P : Measure Ω) [IsProbabilityMeasure P] (ν : Measure X) [IsProbabilityMeasure ν]
    (H : Ω × X → ℝ) (hH : Measurable H)
    (he : ∀ᵐ ω ∂P, Integrable (fun x => Real.exp (H (ω,x))) ν)
    (D₂ : Ω × (Fin 2 → X) → ℝ) (hD₂ : Measurable D₂)
    (D₃ : Ω × (Fin 3 → X) → ℝ) (hD₃ : Measurable D₃)
    {B₂ B₃ : ℝ} (hB₂ : 0 ≤ B₂) (hB₃ : 0 ≤ B₃)
    (hb₂ : ∀ z, |D₂ z| ≤ B₂) (hb₃ : ∀ z, |D₃ z| ≤ B₃)
    {S : ℕ → Set X} (hS : ∀ n, MeasurableSet (S n))
    (hexh : ∀ x, ∀ᶠ n in atTop, x ∈ S n) (hpos : ∀ n, ν (S n) ≠ 0)
    {ε : ℝ} (hfinite : ∀ n,
…