OAI/Probability/SLE/Geometry/MarkedHookLocal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complete marked hook has exactly its two adjacent legs in a small corner-chart neighbourhood. A separated preceding guide contributes no other local intersection.

  1. lemma OAI.SLEExactGauge.Serpentine.markedCornerChart_real_iff line 14
  2. lemma OAI.SLEExactGauge.Serpentine.markedHook_in_small_corner line 28
  3. lemma OAI.SLEExactGauge.Serpentine.markedHook_contains_small_real line 66
  4. theorem OAI.SLEExactGauge.Serpentine.markedHook_small_corner_iff line 88

    Source documentation

    The local intersection statement needed to straighten the complete guide.

    theorem markedHook_small_corner_iff {w z : ℂ} {R H a δ : ℝ}
    (hR : w.re < R) (hH : w.im < H) (ha : 0 < a) (hδ : 0 < δ)
    (hδH : 3 * δ < H - w.im) (hδa : 3 * δ < a) (hz : ‖z‖ < δ) :
    (∃ t : ℝ, 0 ≤ t ∧ markedHook w R H a t = markedCornerChart w z) ↔ z.im = 0 := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.markedHook, OAI.SLEExactGauge.Serpentine.markedCornerChart

  5. lemma OAI.SLEExactGauge.Serpentine.separated_prefix_outside_corner line 97