Curve Avoidance API

General-purpose lemmas for proving that curves avoid points, computing minimum distances, and establishing slitPlane membership for shifted curves.

Main definitions

• CurveAvoids - a curve on [a,b] avoids a point z₀
• curveInfDist - infimum distance from z₀ to the curve image on [a,b]

Main results

• curveInfDist_pos_of_avoids - positive inf distance when curve avoids z₀
• curveAvoids_of_im_pos - curve with positive imaginary part avoids real points
• curve_sub_in_slitPlane - shifted curve lands in slitPlane

def CurveAvoids (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : Prop

A continuous curve on [a,b] avoids a point z₀.

Equations

• CurveAvoids γ a b z₀ = ∀ t ∈ Set.Icc a b, γ t ≠ z₀

noncomputable def curveInfDist (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : ℝ

Infimum distance from z₀ to the curve image on [a,b].

Equations

• curveInfDist γ a b z₀ = Metric.infDist z₀ (γ '' Set.Icc a b)

Basic avoidance criteria

theorem curveAvoids_of_ne_on_Icc {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : ∀ t ∈ Set.Icc a b, γ t ≠ z₀) : CurveAvoids γ a b z₀

Trivial wrapper: CurveAvoids follows from pointwise inequality.

theorem curveAvoids_of_im_lt {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : ∀ t ∈ Set.Icc a b, z₀.im < (γ t).im) : CurveAvoids γ a b z₀

If every point on the curve has imaginary part strictly greater than z₀.im, then the curve avoids z₀.

theorem curveAvoids_of_re_ne {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : ∀ t ∈ Set.Icc a b, (γ t).re ≠ z₀.re) : CurveAvoids γ a b z₀

If every point on the curve has real part different from z₀.re, then the curve avoids z₀.

theorem curveAvoids_of_norm_ne {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : ∀ t ∈ Set.Icc a b, ‖γ t‖ ≠ ‖z₀‖) : CurveAvoids γ a b z₀

If every point on the curve has norm different from ‖z₀‖, then the curve avoids z₀. Useful for curves on circles.

Positive inf-distance

theorem curveInfDist_pos_of_avoids {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (hγ : ContinuousOn γ (Set.Icc a b)) (hab : a ≤ b) (hav : CurveAvoids γ a b z₀) : 0 < curveInfDist γ a b z₀

If a continuous curve on [a,b] with a ≤ b avoids z₀, then the infimum distance from z₀ to the curve image is positive.

slitPlane membership

theorem curve_sub_in_slitPlane {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (_hγ : ContinuousOn γ (Set.Icc a b)) (_hav : CurveAvoids γ a b z₀) (hpos : ∀ t ∈ Set.Icc a b, 0 < (γ t - z₀).im ∨ 0 < (γ t - z₀).re) (t : ℝ) : t ∈ Set.Icc a b → γ t - z₀ ∈ Complex.slitPlane

If a continuous curve avoids z₀ and every shifted value γ t - z₀ has positive imaginary part or positive real part, then every shifted value lies in the slit plane.