OAI/Probability/InvariantIsing/Arrays/OverlapPathCompact.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Sequential L1 compactness of bounded monotone overlap paths. The proof extracts the values on the rationals and discards only the countable discontinuity set of the resulting monotone path.

  1. def OAI.InvariantIsing.rationalLowerValues line 15
  2. lemma OAI.InvariantIsing.rationalLowerValues_nonempty line 18
  3. lemma OAI.InvariantIsing.rationalLowerValues_bdd line 23
  4. def OAI.InvariantIsing.rationalLowerPath line 29
  5. lemma OAI.InvariantIsing.rational_le_lowerPath line 44
  6. lemma OAI.InvariantIsing.rationalLowerPath_tendsto line 48
  7. theorem OAI.InvariantIsing.overlapPath_ae_l1_subsequence line 79

    Source documentation

    Every sequence of overlap quantiles has an L1-convergent subsequence with another admissible bounded monotone representative.

    theorem overlapPath_ae_l1_subsequence (p : ℕ → OverlapPath) :
    ∃ q : OverlapPath, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      (∀ᵐ s ∂pathMeasure, Tendsto (fun n => p (φ n) s) atTop (𝓝 (q s))) ∧
      Tendsto (fun n => ∫ s, |p (φ n) s - q s| ∂pathMeasure) atTop (𝓝 0) := by
…

    Mentions: OAI.InvariantIsing.OverlapPath

  8. theorem OAI.InvariantIsing.overlapPath_l1_subsequence line 109