MultipointLocalization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A finite localization for the completion-frozen logarithmic coordinates. Only the log heights and the real driver are cut off; the smooth factors need no angular cutoff.

def OAI.SLEExactGauge.Multipoint.localizationMarginTerm line 16
def OAI.SLEExactGauge.Multipoint.localizationMargin line 23
Source documentation
The extra none index is the driver margin, so empty point families are allowed without an artificial height condition.
```
def localizationMargin {ι : Type*} [Fintype ι] (lo hi M : ℝ)
    (q : ι → ℂ × ℝ) (b : ℝ) : ℝ :=
…
```
Mentions: OAI.SLEExactGauge.Multipoint.q
lemma OAI.SLEExactGauge.Multipoint.localizationMargin_nonneg_iff line 27
lemma OAI.SLEExactGauge.Multipoint.localizationMargin_pos_iff line 45
lemma OAI.SLEExactGauge.Multipoint.localizationMargin_continuous line 63
lemma OAI.SLEExactGauge.Multipoint.localizationMargin_boundary line 77

theorem OAI.SLEExactGauge.Multipoint.exists_multipoint_localization line 104

Source documentation

Stop the continuous adapted state at the first height or driver boundary, capped at the deterministic horizon.

theorem exists_multipoint_localization
    {Ω ι : Type*} [mΩ : MeasurableSpace Ω] [Fintype ι]
    (ℱ : Filtration ℝ≥0 mΩ)
    (Q : ℝ → Ω → ι → ℂ × ℝ) (B : ℝ≥0 → Ω → ℝ)
    (hQa : Adapted ℱ (fun t : ℝ≥0 => Q t))
    (hQc : ∀ ω, Continuous (fun t : ℝ => Q t ω))
    (hBa : Adapted ℱ B) (hBc : ∀ ω, Continuous (fun t => B t ω))
    (lo hi M : ℝ) (H : ℝ≥0)
    (hQ0 : ∀ ω i, lo ≤ (Q 0 ω i).1.im ∧ (Q 0 ω i).1.im ≤ hi)
    (hB0 : ∀ ω, |B 0 ω| ≤ M) :
    ∃ χ : Ω → ℝ≥0,
      IsStoppingTime ℱ (fun ω => (χ ω : WithTop ℝ≥0)) ∧
…