LocalCrosscutSides.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Opposite local sides of a straightened crosscut. This is a deterministic consequence of disk-image openness and the intermediate value theorem. It does not assume any classification of ribbon exits or harmonic measures.

theorem OAI.SLEExactGauge.CrosscutSides.positive_on_preconnected_of_nonzero line 15
theorem OAI.SLEExactGauge.CrosscutSides.negative_on_preconnected_of_nonzero line 25

theorem OAI.SLEExactGauge.CrosscutSides.opposite_half_disk_signs line 37

Source documentation

An open image of a disk cannot send both sides of its horizontal diameter into the same side of the vertical axis. The zero-set assumption is exactly the assertion that this diameter is the local crosscut.

theorem opposite_half_disk_signs
    (f : ℂ → ℂ) (x : ℂ) {r : ℝ} (hr : 0 < r)
    (hf : ContinuousOn f (ball x r)) (ho : IsOpen (f '' ball x r))
    (hfx : (f x).re = 0)
    (hz : ∀ z ∈ ball x r, (f z).re = 0 ↔ z.im = 0) :
    ((∀ z ∈ ball x r, 0 < z.im → 0 < (f z).re) ∧
      (∀ z ∈ ball x r, z.im < 0 → (f z).re < 0)) ∨
    ((∀ z ∈ ball x r, 0 < z.im → (f z).re < 0) ∧
      (∀ z ∈ ball x r, z.im < 0 → 0 < (f z).re)) := by
…