OAI/Probability/SLE/Gauge/CoverMesh.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The deterministic common mesh in the dense-cover construction. At each stage there are only finitely many positive test cutoffs. The mesh satisfies every cutoff and decreases by at least a factor of two at each stage.

  1. def OAI.SLEExactGauge.CoverMesh.cutoff line 17
  2. lemma OAI.SLEExactGauge.CoverMesh.cutoff_pos line 21
  3. lemma OAI.SLEExactGauge.CoverMesh.cutoff_le_one line 31
  4. lemma OAI.SLEExactGauge.CoverMesh.cutoff_le_test line 36
  5. def OAI.SLEExactGauge.CoverMesh.mesh line 42
  6. lemma OAI.SLEExactGauge.CoverMesh.mesh_pos line 46
  7. lemma OAI.SLEExactGauge.CoverMesh.mesh_half line 53
  8. lemma OAI.SLEExactGauge.CoverMesh.mesh_le_cutoff line 56
  9. lemma OAI.SLEExactGauge.CoverMesh.mesh_le_test line 62
  10. lemma OAI.SLEExactGauge.CoverMesh.mesh_le_half_pow line 66
  11. lemma OAI.SLEExactGauge.CoverMesh.mesh_le_dyadic line 76
  12. lemma OAI.SLEExactGauge.CoverMesh.mesh_tendsto_zero line 82
  13. theorem OAI.SLEExactGauge.CoverMesh.exists_common_mesh line 90

    Source documentation

    One positive deterministic mesh works for every finite test window, including empty windows, and tends to zero with geometric decay.

    theorem exists_common_mesh (I : ℕ → Finset ℕ) (ε : ℕ → ℕ → ℝ)
    (hε : ∀ n i, i ∈ I n → 0 < ε n i) :
    ∃ v : ℕ → ℝ, (∀ n, 0 < v n) ∧
      (∀ n, v n ≤ (2 : ℝ) ^ (-(n : ℝ))) ∧
      (∀ n, v (n + 1) ≤ v n / 2) ∧
      (∀ n i, i ∈ I n → v n ≤ ε n i) ∧ Tendsto v atTop (𝓝 0) :=
…