The Jordan index theorem and orientation sign for absolutely continuous and rectifiable curves

For a simple closed absolutely continuous curve γ on [a, b] (a < b, γ a = γ b, InjOn γ (Ico a b)), the trace C = γ '' uIcc a b is a planar Jordan curve. Its complement splits into two connected components: the bounded inside Ω = filledHull C \ C and the unbounded outside (filledHull C)ᶜ (where windingNumber γ a b vanishes for any closed AC curve by AbsolutelyContinuousOnInterval.windingNumber_eq_zero_of_notMem_filledHull).

This file defines the canonical orientation sign TauCeti.Contour.jordanSign γ a b : ℤ and proves the Jordan index theorem:

1. jordanSign γ a b ∈ {1, -1} (AbsolutelyContinuousOnInterval.jordanSign_eq_one_or_neg_one), and
2. windingNumber γ a b z = jordanSign γ a b for every z ∈ filledHull C \ C (AbsolutelyContinuousOnInterval.windingNumber_eq_jordanSign_of_mem_filledHull_sdiff).

At every interior parameter t₀ ∈ (a, b) where γ is differentiable with nonzero velocity v ≠ 0, jordanSign γ a b identifies the geometric normal orientation: the rotated vector (jordanSign γ a b : ℝ) • (I * v) points strictly into Ω, while its negation -(jordanSign γ a b : ℝ) • (I * v) points strictly into (filledHull C)ᶜ (AbsolutelyContinuousOnInterval.eventually_mem_filledHull_sdiff_and_notMem_of_hasDerivAt).

We also record the reversal and monotone/antitone reparametrization laws of jordanSign, evaluate jordanSign (circleMap c R) 0 (2 * π) = 1 for every R ≠ 0, and specialize the Jordan index theorem and continuous reparametrization laws to the arclength parametrization naturalParameterization γ (Icc a b) a of any rectifiable simple closed curve.

References

• L. Ahlfors, Complex Analysis, Chapter 4, §2.
• R. B. Burckel, An Introduction to Classical Complex Analysis, Vol. 1, Chapter IV & Chapter IX.

Definition and elementary properties of jordanSign

noncomputable def TauCeti.Contour.jordanSign (γ : ℝ → ℂ) (a b : ℝ) : ℤ

The orientation sign of a planar curve γ on [a, b]: equal to 1 (resp. -1) when the bounded inside filledHull (γ '' uIcc a b) \ (γ '' uIcc a b) is nonempty and windingNumber γ a b is constantly 1 (resp. -1) there, and 0 otherwise.

For a simple closed absolutely continuous curve with a < b, the Jordan index theorem proves that jordanSign γ a b is always 1 or -1 and equals the winding number throughout the inside.

theorem TauCeti.Contour.jordanSign_def (γ : ℝ → ℂ) (a b : ℝ) : jordanSign γ a b = if (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).Nonempty ∧ ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, windingNumber γ a b z = 1 then 1 else if (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).Nonempty ∧ ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, windingNumber γ a b z = -1 then -1 else 0

Defining formula for TauCeti.Contour.jordanSign.

@[simp]

theorem TauCeti.Contour.jordanSign_eq_one_iff {γ : ℝ → ℂ} {a b : ℝ} : jordanSign γ a b = 1 ↔ (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).Nonempty ∧ ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, windingNumber γ a b z = 1

jordanSign γ a b = 1 if and only if the bounded inside is nonempty and windingNumber γ a b is constantly 1 on it.

@[simp]

theorem TauCeti.Contour.jordanSign_eq_neg_one_iff {γ : ℝ → ℂ} {a b : ℝ} : jordanSign γ a b = -1 ↔ (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).Nonempty ∧ ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, windingNumber γ a b z = -1

jordanSign γ a b = -1 if and only if the bounded inside is nonempty and windingNumber γ a b is constantly -1 on it.

theorem TauCeti.Contour.jordanSign_of_windingNumber_eq_one {γ : ℝ → ℂ} {a b : ℝ} (hne : (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).Nonempty) (h : ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, windingNumber γ a b z = 1) : jordanSign γ a b = 1

If the bounded inside is nonempty and windingNumber γ a b is 1 throughout it, then jordanSign γ a b = 1.

theorem TauCeti.Contour.jordanSign_of_windingNumber_eq_neg_one {γ : ℝ → ℂ} {a b : ℝ} (hne : (filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).Nonempty) (h : ∀ z ∈ filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, windingNumber γ a b z = -1) : jordanSign γ a b = -1

If the bounded inside is nonempty and windingNumber γ a b is -1 throughout it, then jordanSign γ a b = -1.

theorem TauCeti.Contour.jordanSign_eq_one_or_neg_one_or_zero (γ : ℝ → ℂ) (a b : ℝ) : jordanSign γ a b = 1 ∨ jordanSign γ a b = -1 ∨ jordanSign γ a b = 0

Every value of jordanSign belongs to {1, -1, 0}.

theorem TauCeti.Contour.abs_jordanSign_le_one (γ : ℝ → ℂ) (a b : ℝ) : |jordanSign γ a b| ≤ 1

The absolute value of jordanSign never exceeds 1.

theorem TauCeti.Contour.jordanSign_congr {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} (h : Set.EqOn γ₁ γ₂ (Set.uIcc a b)) : jordanSign γ₁ a b = jordanSign γ₂ a b

jordanSign depends only on the values of the curve on uIcc a b.

@[simp]

theorem TauCeti.Contour.jordanSign_same (γ : ℝ → ℂ) (a : ℝ) : jordanSign γ a a = 0

On a degenerate interval [a, a], jordanSign vanishes.

@[simp]

theorem TauCeti.Contour.jordanSign_const (c : ℂ) (a b : ℝ) : jordanSign (fun (x : ℝ) => c) a b = 0

A constant curve has jordanSign equal to 0.

Reparametrization laws and Jordan index theorem for AC curves

theorem AbsolutelyContinuousOnInterval.jordanSign_symm {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : TauCeti.Contour.jordanSign γ b a = -TauCeti.Contour.jordanSign γ a b

Reversing the interval orientation negates jordanSign.

theorem AbsolutelyContinuousOnInterval.jordanSign_comp_of_monotoneOn {γ : ℝ → ℂ} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (Set.Icc a b)) (ha : θ a = c) (hb : θ b = d) : TauCeti.Contour.jordanSign (γ ∘ θ) a b = TauCeti.Contour.jordanSign γ c d

An increasing absolutely continuous reparametrization onto [c, d] preserves jordanSign.

theorem AbsolutelyContinuousOnInterval.jordanSign_comp_of_antitoneOn {γ : ℝ → ℂ} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hanti : AntitoneOn θ (Set.Icc a b)) (ha : θ a = d) (hb : θ b = c) : TauCeti.Contour.jordanSign (γ ∘ θ) a b = -TauCeti.Contour.jordanSign γ c d

A decreasing absolutely continuous reparametrization onto [c, d] negates jordanSign.

@[simp]

theorem AbsolutelyContinuousOnInterval.jordanSign_comp_lineMap {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : TauCeti.Contour.jordanSign (γ ∘ ⇑(AffineMap.lineMap a b)) 0 1 = TauCeti.Contour.jordanSign γ a b

Affine normalization to [0, 1] preserves jordanSign, carrying the orientation of the original ordered pair (a, b).

theorem AbsolutelyContinuousOnInterval.jordanSign_comp_sub {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : TauCeti.Contour.jordanSign (fun (t : ℝ) => γ (a + b - t)) a b = -TauCeti.Contour.jordanSign γ a b

Parameter reflection t ↦ γ (a + b - t) on [a, b] negates jordanSign.

theorem AbsolutelyContinuousOnInterval.jordanSign_eq_one_or_neg_one {γ : ℝ → ℂ} {a b : ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) : TauCeti.Contour.jordanSign γ a b = 1 ∨ TauCeti.Contour.jordanSign γ a b = -1

Jordan index theorem (orientation sign dichotomy): for a simple closed absolutely continuous curve on [a, b] (a < b), jordanSign γ a b is either 1 or -1, and equals the winding number at every point of filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).

@[simp]

theorem AbsolutelyContinuousOnInterval.abs_jordanSign_eq_one {γ : ℝ → ℂ} {a b : ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) : |TauCeti.Contour.jordanSign γ a b| = 1

The orientation sign of a simple closed absolutely continuous curve (a < b) has unit absolute value.

theorem AbsolutelyContinuousOnInterval.jordanSign_ne_zero {γ : ℝ → ℂ} {a b : ℝ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) : TauCeti.Contour.jordanSign γ a b ≠ 0

The orientation sign of a simple closed absolutely continuous curve (a < b) is nonzero.

theorem AbsolutelyContinuousOnInterval.windingNumber_eq_jordanSign_of_mem_filledHull_sdiff {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (hz : z ∈ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b) : TauCeti.Contour.windingNumber γ a b z = ↑(TauCeti.Contour.jordanSign γ a b)

The Jordan index theorem for simple closed absolutely continuous curves: on the bounded inside filledHull (γ '' uIcc a b) \ (γ '' uIcc a b), windingNumber γ a b is constantly equal to jordanSign γ a b ∈ {1, -1}.

theorem AbsolutelyContinuousOnInterval.eventually_mem_filledHull_sdiff_and_notMem_of_hasDerivAt {γ : ℝ → ℂ} {a b t₀ : ℝ} {v : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (ht₀ : t₀ ∈ Set.Ioo a b) (hd : HasDerivAt γ v t₀) (hv : v ≠ 0) : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ t₀ + h • ↑(TauCeti.Contour.jordanSign γ a b) • (Complex.I * v) ∈ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b ∧ γ t₀ - h • ↑(TauCeti.Contour.jordanSign γ a b) • (Complex.I * v) ∉ TauCeti.filledHull (γ '' Set.uIcc a b)

Geometric normal identification of jordanSign: at any interior parameter t₀ ∈ (a, b) where a simple closed absolutely continuous curve has nonzero derivative v ≠ 0, the vector (jordanSign γ a b : ℝ) • (I * v) points into the bounded inside filledHull (γ '' uIcc a b) \ (γ '' uIcc a b), while -(jordanSign γ a b : ℝ) • (I * v) points into the unbounded outside (filledHull (γ '' uIcc a b))ᶜ.

theorem AbsolutelyContinuousOnInterval.jordanSign_eq_one_iff_eventually_mem_filledHull_sdiff {γ : ℝ → ℂ} {a b t₀ : ℝ} {v : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (ht₀ : t₀ ∈ Set.Ioo a b) (hd : HasDerivAt γ v t₀) (hv : v ≠ 0) : TauCeti.Contour.jordanSign γ a b = 1 ↔ ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ t₀ + h • (Complex.I * v) ∈ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b

At any regular interior point t₀ ∈ (a, b) (HasDerivAt γ v t₀, v ≠ 0), a simple closed AC curve is positively oriented (jordanSign γ a b = 1) if and only if the leftward normal I * v points into the bounded inside filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).

theorem AbsolutelyContinuousOnInterval.jordanSign_eq_neg_one_iff_eventually_mem_filledHull_sdiff {γ : ℝ → ℂ} {a b t₀ : ℝ} {v : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (ht₀ : t₀ ∈ Set.Ioo a b) (hd : HasDerivAt γ v t₀) (hv : v ≠ 0) : TauCeti.Contour.jordanSign γ a b = -1 ↔ ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ t₀ - h • (Complex.I * v) ∈ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b

Counterpart of jordanSign_eq_one_iff_eventually_mem_filledHull_sdiff for negative orientation (jordanSign γ a b = -1): -(I * v) points into the bounded inside.

theorem AbsolutelyContinuousOnInterval.jordanSign_naturalParameterization {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a ≤ b) : TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal = TauCeti.Contour.jordanSign γ a b

Arclength invariance of jordanSign for absolutely continuous curves: for a ≤ b, passing to naturalParameterization γ (Icc a b) a on [0, (eVariationOn γ (Icc a b)).toReal] preserves jordanSign.

Concrete evaluation on circles

@[simp]

theorem TauCeti.Contour.jordanSign_circleMap (c : ℂ) {R : ℝ} (hR : R ≠ 0) : jordanSign (circleMap c R) 0 (2 * Real.pi) = 1

The standard circle circleMap c R (R ≠ 0) on [0, 2π] has orientation sign 1.

@[simp]

theorem TauCeti.Contour.jordanSign_circleMap_symm (c : ℂ) {R : ℝ} (hR : R ≠ 0) : jordanSign (circleMap c R) (2 * Real.pi) 0 = -1

The reversed circle circleMap c R (R ≠ 0) on [2π, 0] has orientation sign -1.

Arclength specialization and continuous reparametrization laws for rectifiable curves

theorem BoundedVariationOn.jordanSign_naturalParameterization_eq_one_or_neg_one {γ : ℝ → ℂ} {a b : ℝ} (hab : a < b) (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) : TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal = 1 ∨ TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal = -1

Jordan index theorem for rectifiable simple closed curves (orientation sign dichotomy): the arclength parametrization naturalParameterization γ (Icc a b) a on [0, (eVariationOn γ (Icc a b)).toReal] of a continuous simple closed curve of bounded variation (a < b) has orientation sign 1 or -1.

theorem BoundedVariationOn.windingNumber_naturalParameterization_eq_jordanSign {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hab : a < b) (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) (hz : z ∈ TauCeti.filledHull (γ '' Set.Icc a b) \ γ '' Set.Icc a b) : TauCeti.Contour.windingNumber (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal z = ↑(TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal)

The Jordan index theorem for the arclength parametrization of a rectifiable simple closed curve: on filledHull (γ '' Icc a b) \ (γ '' Icc a b), the winding number of naturalParameterization γ (Icc a b) a equals its orientation sign σ ∈ {1, -1}.

theorem BoundedVariationOn.jordanSign_naturalParameterization_comp_of_monotoneOn {γ : ℝ → ℂ} {φ : ℝ → ℝ} {a b c d : ℝ} (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc c d)) (hφm : MonotoneOn φ (Set.Icc c d)) (hφc : φ c = a) (hφd : φ d = b) : TauCeti.Contour.jordanSign (naturalParameterization (γ ∘ φ) (Set.Icc c d) c) 0 (eVariationOn (γ ∘ φ) (Set.Icc c d)).toReal = TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal

Increasing continuous reparametrizations preserve the arclength orientation sign of a rectifiable curve. The reparametrization φ need not be absolutely continuous.

theorem BoundedVariationOn.jordanSign_naturalParameterization_comp_of_antitoneOn {γ : ℝ → ℂ} {φ : ℝ → ℝ} {a b c d : ℝ} (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc c d)) (hφm : AntitoneOn φ (Set.Icc c d)) (hφc : φ c = b) (hφd : φ d = a) : TauCeti.Contour.jordanSign (naturalParameterization (γ ∘ φ) (Set.Icc c d) c) 0 (eVariationOn (γ ∘ φ) (Set.Icc c d)).toReal = -TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal

Decreasing continuous reparametrizations negate the arclength orientation sign of a rectifiable curve. The reparametrization φ need not be absolutely continuous.