OAI/Probability/InvariantIsing/Cavity/CavityRoundedSelfConsistency.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The cavity identity is initially tested at the rounded overlap. Passing those tests to the limiting overlap gives the L1 conclusion.

  1. lemma OAI.InvariantIsing.cavity_rounding_test_difference line 14
  2. theorem OAI.InvariantIsing.cavity_rounded_self_consistency_l1 line 69
  3. theorem OAI.InvariantIsing.cavity_rounded_self_consistency_l1_on line 83

    Source documentation

    Finite-grid endpoints may be removed from a common full-measure set; ties there suffice for the actual rounded cavity fields.

    theorem cavity_rounded_self_consistency_l1_on (p : OverlapPath)
    (q B : ℕ → OverlapPath)
    (hq : ∀ᵐ s ∂pathMeasure, Tendsto (fun n => q n s) atTop (𝓝 (p s)))
    (D : Set ℝ) (hDae : ∀ᵐ s ∂pathMeasure, s ∈ D)
    (htied : ∀ n x, x ∈ D → ∀ y, y ∈ D → p x = p y → B n x = B n y)
    (htest : ∀ Φ : ℝ →ᵇ ℝ, Tendsto
      (fun n => ∫ s, Φ (q n s) * (B n s - q n s) ∂pathMeasure) atTop (𝓝 0)) :
    Tendsto (fun n => ∫ s, |B n s - p s| ∂pathMeasure) atTop (𝓝 0) := by
…

    Mentions: OAI.InvariantIsing.OverlapPath