OAI/Probability/SLE/Gauge/DenseRibbonNumerics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absorb the fixed initial passage probability into the quadratic experiment cost, and convert width-scaled unit-strip mass to m^(2-d).

  1. lemma OAI.SLEExactGauge.ribbon_mass_after_width_scaling line 14
  2. theorem OAI.SLEExactGauge.ribbon_initial_and_steps_quadratic_cost line 25

    Source documentation

    One initial positive-probability event and quadratically many uniform steps have one stretched-exponential cost, uniformly in the mesh.

    theorem ribbon_initial_and_steps_quadratic_cost
    {q p D : ℝ} (hq : 0 < q) (hq1 : q ≤ 1)
    (hp : 0 < p) (hD : 0 ≤ D) :
    ∃ C : ℝ, 0 < C ∧ ∀ (m N : ℕ), 0 < m → (N : ℝ) ≤ D * (m : ℝ) ^ 2 →
      Real.exp (-C * (m : ℝ) ^ 2) ≤ q ^ N * p := by
…