RobustTransverseCrossing.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Rectangle separation remains valid for a perturbed transverse route: its ends may lie beyond the narrow core, with no regularity of the past.

theorem OAI.SLEExactGauge.RectangleCrossing.transverse_crossing_beyond_edges_hits_past line 14
def OAI.SLEExactGauge.RectangleCrossing.transverseTemplate line 35

theorem OAI.SLEExactGauge.RectangleCrossing.near_transverse_template_hits_past line 40

Source documentation

A fixed coordinate tube around the transverse segment forces a hit of any continuous past crossing the ribbon's narrow core.

theorem near_transverse_template_hits_past
    (p q : ℝ → ℂ) {T k ε δ : ℝ} (hT : 0 < T) (hk : 1 ≤ k)
    (hε : 0 < ε) (hεsmall : ε ≤ 1 / 8) (hδ : δ ≤ 1 / 8)
    (hp : ContinuousOn p (Icc 0 T)) (hq : ContinuousOn q (Icc 0 1))
    (hp0 : (p 0).re = 0) (hpT : (p T).re = k)
    (hpim : ∀ t ∈ Icc (0 : ℝ) T, |(p t).im| ≤ ε)
    (hnear : ∀ t ∈ Icc (0 : ℝ) 1, dist (q t) (transverseTemplate k t) < δ) :
    ∃ s ∈ Icc (0 : ℝ) T, ∃ t ∈ Icc (0 : ℝ) 1, p s = q t := by
…

Mentions: OAI.SLEExactGauge.RectangleCrossing.transverseTemplate