OAI/Probability/InvariantIsing/Cavity/CavityFiberFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tied overlap levels remain tied in an almost-everywhere limit. A monotone factor through the overlap is then constructed explicitly; no invertibility or absence of plateaus is assumed.

  1. def OAI.InvariantIsing.cavityFiberValues line 15
  2. lemma OAI.InvariantIsing.cavityFiberValues_bdd line 18
  3. lemma OAI.InvariantIsing.cavityFiberFactor_mono line 25
  4. lemma OAI.InvariantIsing.cavityFiberFactor_bounds line 33
  5. lemma OAI.InvariantIsing.cavityFiberFactor_eq line 42
  6. theorem OAI.InvariantIsing.cavity_limit_factors_through_overlap_on line 58

    Source documentation

    An a.e. limit of functions constant on every overlap fiber is still a measurable function of that overlap, even on positive-mass plateaus.

    theorem cavity_limit_factors_through_overlap_on (p B : OverlapPath) (Bseq : ℕ → ℝ → ℝ)
    (D : Set ℝ) (hDae : ∀ᵐ s ∂pathMeasure, s ∈ D)
    (htied : ∀ n x, x ∈ D → ∀ y, y ∈ D → p x = p y → Bseq n x = Bseq n y)
    (hlim : ∀ᵐ s ∂pathMeasure, Tendsto (fun n => Bseq n s) atTop (𝓝 (B s))) :
    ∃ g : ℝ → ℝ, Monotone g ∧ (∀ z, 0 ≤ g z ∧ g z ≤ 1) ∧
      B.val =ᵐ[pathMeasure] fun s => g (p s) := by
…

    Mentions: OAI.InvariantIsing.OverlapPath

  7. theorem OAI.InvariantIsing.cavity_limit_factors_through_overlap line 75