Uniform distance from an avoided point to a continuous curve

For a curve γ : ℝ → ℂ continuous on a compact interval [a, b] and avoiding a point w, the image γ '' [a, b] is compact and misses w, so w stays a positive distance from it; this gives a uniform positive lower bound ρ on ‖γ t - w‖ over [a, b].

Main results

• TauCeti.Contour.exists_curve_dist_lower_bound — the uniform positive distance lower bound.
• TauCeti.Contour.exists_ball_dist_curve_lower_bound — the same lower bound made uniform over a whole ball of points around the avoided point.
• TauCeti.Contour.exists_mem_off_curve — an open set containing a curve contains a point off the curve: the compact image cannot exhaust a nonempty open subset of the noncompact connected ℂ.
• TauCeti.Contour.isClosed_setOfPred_mem_uIcc_dist_le and its norm spelling TauCeti.Contour.isClosed_setOfPred_mem_uIcc_norm_sub_le — the parameters at which a curve stays within ε of a point form a closed set. Where the lemmas above give lower bounds on the distance to an avoided point, this one describes the near-point parameter set itself, which is what the excision arguments of the principal-value theory need.

These small support lemmas are shared by the argument-lift partition (exists_uniform_modulus_avoiding, feeding the integer-valuedness of the winding number), by the continuity of the winding number in the point (continuousAt_windingNumber_of_avoidance), and by the homology form of Cauchy's theorem (homologyCauchyTheorem), whose Dixon-style proof picks its base point off the curve via exists_mem_off_curve.

theorem TauCeti.Contour.exists_curve_dist_lower_bound {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} (hγ : ContinuousOn γ (Set.uIcc a b)) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) : ∃ ρ > 0, ∀ t ∈ Set.uIcc a b, ρ ≤ ‖γ t - w‖

Uniform positive distance from an avoided point to a curve. If γ is continuous on the interval with endpoints a, b and avoids w there, then there is ρ > 0 with ρ ≤ ‖γ t - w‖ for every t ∈ Set.uIcc a b (one may take ρ = Metric.infDist w (γ '' Set.uIcc a b)). Stated on the oriented interval Set.uIcc a b, matching the winding-number API.

theorem TauCeti.Contour.exists_ball_dist_curve_lower_bound {γ : ℝ → ℂ} {w₀ : ℂ} {a b : ℝ} (hγ : ContinuousOn γ (Set.uIcc a b)) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w₀) : ∃ ε > 0, ∀ w ∈ Metric.ball w₀ ε, ∀ t ∈ Set.uIcc a b, ε ≤ ‖γ t - w‖

Uniform distance to the curve on a neighbourhood of an avoided point. If γ is continuous on the interval with endpoints a, b and avoids w₀ there, then there is a radius ε > 0 such that every w within ε of w₀ stays at distance at least ε from the whole curve: for all t ∈ Set.uIcc a b, ε ≤ ‖γ t - w‖. Stated on the oriented interval Set.uIcc a b.

theorem TauCeti.Contour.exists_mem_off_curve {γ : ℝ → ℂ} {Ω : Set ℂ} {a b : ℝ} (hΩ : IsOpen Ω) (hγ : ContinuousOn γ (Set.uIcc a b)) (hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) : ∃ w₀ ∈ Ω, ∀ t ∈ Set.uIcc a b, γ t ≠ w₀

An open set containing a curve contains a point off the curve. If γ is continuous on the interval with endpoints a, b and maps it into an open set Ω ⊆ ℂ, then some w₀ ∈ Ω is not on the curve. The image is compact, so if it exhausted Ω then Ω would be a nonempty clopen subset of the connected ℂ, hence all of ℂ — which is not compact. This supplies the base point off the curve that Dixon's proof of the homology Cauchy theorem requires.

theorem TauCeti.Contour.isClosed_setOfPred_mem_uIcc_dist_le {E : Type u_1} [PseudoMetricSpace E] {γ : ℝ → E} {a b : ℝ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (s : E) (ε : ℝ) : IsClosed {t : ℝ | t ∈ Set.uIcc a b ∧ dist (γ t) s ≤ ε}

The set where a curve stays near a point is closed. For a curve continuous on [[a, b]] into a pseudo metric space, the set of parameters at which it stays within ε of a point s is closed.

theorem TauCeti.Contour.isClosed_setOfPred_mem_uIcc_norm_sub_le {E : Type u_1} [SeminormedAddCommGroup E] {γ : ℝ → E} {a b : ℝ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (s : E) (ε : ℝ) : IsClosed {t : ℝ | t ∈ Set.uIcc a b ∧ ‖γ t - s‖ ≤ ε}

The norm spelling of isClosed_setOfPred_mem_uIcc_dist_le, which is the form the contour arguments use.