OAI/Probability/InvariantIsing/Cavity/CavityMeasurableTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous overlap tests determine a bounded measurable residual once it is known to be a function of that overlap.

  1. theorem OAI.InvariantIsing.cavity_ae_zero_of_measurable_overlap_tests line 15
  2. theorem OAI.InvariantIsing.cavity_overlap_self_consistency line 71

    Source documentation

    This is the separation step in cavity self-consistency, including positive-mass plateaus of the limiting total-overlap path.

    theorem cavity_overlap_self_consistency (p B : OverlapPath) (g : ℝ → ℝ)
    (hg : Monotone g) (hgb : ∀ z, 0 ≤ g z ∧ g z ≤ 1)
    (hfactor : B.val =ᵐ[pathMeasure] fun s => g (p s))
    (htest : ∀ Φ : ℝ →ᵇ ℝ, (∫ s, Φ (p s) * (B s - p s) ∂pathMeasure) = 0) :
    B.val =ᵐ[pathMeasure] p.val := by
…

    Mentions: OAI.InvariantIsing.OverlapPath