RibbonExperimentAssembly.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The dense experiment concatenates full passage-and-mass events only on histories where every previous passage has succeeded. Their spatial middle strips are then charged to one actual sausage.

lemma OAI.SLEExactGauge.adapted_successes_lower_bound_on_previous line 17
lemma OAI.SLEExactGauge.ribbon_probability_of_quadratic_completion line 54

theorem OAI.SLEExactGauge.ribbon_experiment_mass_event_probability line 70

Source documentation

The genuine adapted successes force the desired whole-trace mass at one prescribed mesh, using only retained disjoint middle strips.

theorem ribbon_experiment_mass_event_probability
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (μ : Measure Ω)
    (ℱ : Filtration ℕ mΩ) (init : Set Ω) (hinit : MeasurableSet[ℱ 0] init)
    (success : ℕ → Set Ω) (hmeas : ∀ n, MeasurableSet[ℱ (n + 1)] (success n))
    (q : ℝ≥0∞)
    (hstep : ∀ n (A : Set Ω), MeasurableSet[ℱ n] A →
      A ⊆ init ∩ ⋂ j ∈ Finset.range n, success j → q * μ A ≤ μ (A ∩ success n))
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hiP : InjOn P closedRibbon)
    {ε : ℝ} (hε : ε ≤ 1) (I : Finset ℕ) (N : ℕ)
    (κ : ℝ) (γ : Ω → ℝ≥0 → ℂ) (s t : ℕ → Ω → ℝ≥0) (v c ell : ℝ)
    (hell : 0 < ell) (m : ℕ) (hm : 0 < m) (hcard : I.card = m ^ 2) (D : Set ℂ)
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness