RibbonConcatenation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Adapted concatenation and the mass/probability scaling of a serpentine ribbon with a quadratic number of narrow steps.

theorem OAI.SLEExactGauge.adapted_successes_lower_bound line 16

Source documentation

Success probabilities multiply as lower bounds under adapted restarts. The successive steps need not be independent.

theorem adapted_successes_lower_bound
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω)
    (F : Filtration ℕ mΩ) (success : ℕ → Set Ω)
    (hmeas : ∀ n, MeasurableSet[F (n + 1)] (success n))
    (q : ℝ≥0∞)
    (hstep : ∀ n (B : Set Ω), MeasurableSet[F n] B →
      q * P B ≤ P (B ∩ success n)) :
    ∀ N : ℕ, q ^ N * P univ ≤ P (⋂ n ∈ Finset.range N, success n) := by
…

lemma OAI.SLEExactGauge.ribbon_mass_power_cancellation line 51

theorem OAI.SLEExactGauge.ribbon_m_squared_mass_lower line 59

Source documentation

The disjoint middle strips of m² steps of width 1/m carry mass of order m^(2-d), with no dependence assumption in this deterministic sum.

theorem ribbon_m_squared_mass_lower {ι : Type*} (I : Finset ι)
    (ν : Measure ℂ) (D : ι → Set ℂ)
    (hdisj : (I : Set ι).PairwiseDisjoint D)
    (hmeas : ∀ i ∈ I, MeasurableSet (D i))
    (κ : ℝ) (m : ℕ) (hm : 0 < m) (hcard : I.card = m ^ 2)
    (b : ℝ) (_hb : 0 ≤ b)
    (hmass : ∀ i ∈ I, ENNReal.ofReal (b * (1 / (m : ℝ)) ^ dimension κ) ≤ ν (D i)) :
    ENNReal.ofReal (b * (m : ℝ) ^ codimension κ) ≤ ν (⋃ i ∈ I, D i) := by
…

Mentions: OAI.SLEExactGauge.dimension, OAI.SLEExactGauge.codimension

theorem OAI.SLEExactGauge.ribbon_quadratic_probability line 84

Source documentation

A quadratic number of fixed-probability passages has the exponential cost used by the dense visit.

theorem ribbon_quadratic_probability {q : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) :
    ∃ C : ℝ, 0 < C ∧ ∀ m : ℕ,
      Real.exp (-C * (m : ℝ) ^ 2) ≤ q ^ (m ^ 2) := by
…