Proposition 2.2: Finite Crossings and Isolated Crossing Intervals

For a PiecewiseC1Immersion γ : [a,b] → ℂ, we prove that the set of parameter values where γ passes through a given point z₀ is finite. This is Proposition 2.2 from Hungerbuhler-Wasem.

Main Results

• finite_crossings — the set {t ∈ Icc a b | γ t = z₀} is finite
• exists_isolated_crossing_interval — each crossing has an isolating sub-interval

Proof Strategy

At smooth points, HasDerivAt.eventually_ne (from deriv_ne_zero) shows crossings are isolated. At partition points, one-sided derivative limits are nonzero, which also gives isolation on each side via strict monotonicity of a real projection. The crossing set is closed and has no accumulation points, hence finite by compactness.

Helper: HasDerivAt for real part composition

Eventually not in partition (shared pattern)

Isolation of crossings at smooth points

theorem PiecewiseC1Immersion.eventually_ne_at_smooth_crossing (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Icc γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (hsmooth : t₀ ∉ γ.partition) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ {t₀}ᶜ, γ.toFun t ≠ z₀

At a smooth point (not in partition) where γ(t₀) = z₀, there is a punctured neighborhood in which γ(t) ≠ z₀.

Isolation of crossings at partition points

theorem PiecewiseC1Immersion.eventually_ne_left_of_partition (γ : PiecewiseC1Immersion) (z₀ : ℂ) (p : ℝ) (hp : p ∈ γ.partition) (hap : γ.a < p) (hpb : p ≤ γ.b) (hcross : γ.toFun p = z₀) : ∀ᶠ (t : ℝ) in nhdsWithin p (Set.Iio p), γ.toFun t ≠ z₀

At a partition point p with a < p, the left-sided derivative limit is nonzero, so γ(t) ≠ γ(p) for t sufficiently close to p from the left.

theorem PiecewiseC1Immersion.eventually_ne_right_of_partition (γ : PiecewiseC1Immersion) (z₀ : ℂ) (p : ℝ) (hp : p ∈ γ.partition) (hap : γ.a ≤ p) (hpb : p < γ.b) (hcross : γ.toFun p = z₀) : ∀ᶠ (t : ℝ) in nhdsWithin p (Set.Ioi p), γ.toFun t ≠ z₀

At a partition point p with p < b, the right-sided derivative limit is nonzero, so γ(t) ≠ γ(p) for t sufficiently close to p from the right.

Crossings are isolated

theorem PiecewiseC1Immersion.crossing_isolated_nhds (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Icc γ.a γ.b) (hcross : γ.toFun t₀ = z₀) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ {t₀}ᶜ, γ.toFun t ≠ z₀ ∨ t ∉ Set.Icc γ.a γ.b

At any crossing t₀ ∈ [a, b], there is a punctured neighborhood with no other crossings in [a,b].

theorem PiecewiseC1Immersion.crossing_not_accPt (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Icc γ.a γ.b) (hcross : γ.toFun t₀ = z₀) : ¬AccPt t₀ (Filter.principal {t : ℝ | t ∈ Set.Icc γ.a γ.b ∧ γ.toFun t = z₀})

No point of the crossing set is an accumulation point.

theorem crossing_set_isClosed (γ : PiecewiseC1Immersion) (z₀ : ℂ) : IsClosed {t : ℝ | t ∈ Set.Icc γ.a γ.b ∧ γ.toFun t = z₀}

The crossing set is closed.

Main theorem

theorem finite_crossings (γ : PiecewiseC1Immersion) (z₀ : ℂ) : {t : ℝ | t ∈ Set.Icc γ.a γ.b ∧ γ.toFun t = z₀}.Finite

Proposition 2.2: The crossing set is finite.

Isolated crossing intervals

theorem exists_isolated_crossing_interval (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) : ∃ (a' : ℝ) (b' : ℝ), a' < t₀ ∧ t₀ < b' ∧ Set.Icc a' b' ⊆ Set.Icc γ.a γ.b ∧ (∀ t ∈ Set.Icc a' b', γ.toFun t = z₀ → t = t₀) ∧ ∀ t ∈ Set.Ioo a' b', t ∉ γ.partition → DifferentiableAt ℝ γ.toFun t

For each crossing, there exists an isolating sub-interval.

CPV existence for (z - z₀)⁻¹ along piecewise C¹ immersions

theorem PiecewiseC1Immersion.deriv_ne_zero_of_C2 (γ : PiecewiseC1Immersion) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hγ_C2 : ContDiffAt ℝ 2 γ.toFun t₀) : deriv γ.toFun t₀ ≠ 0

theorem cpv_exists_single_crossing (γ : PiecewiseC1Immersion) (z₀ : ℂ) (a' b' t₀ : ℝ) (hat₀ : t₀ ∈ Set.Ioo a' b') (hcross : γ.toFun t₀ = z₀) (h_sub : Set.Icc a' b' ⊆ Set.Icc γ.a γ.b) (h_inj : ∀ t ∈ Set.Icc a' b', γ.toFun t = z₀ → t = t₀) (hγ_C2 : ContDiffAt ℝ 2 γ.toFun t₀) (h_cont_deriv : ContinuousOn (deriv γ.toFun) (Set.Icc a' b')) (hγ_meas : Measurable γ.toFun) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - z₀)⁻¹) γ.toFun a' b' z₀

CPV of (z - z₀)⁻¹ exists on a sub-interval with a single crossing, given C² regularity at the crossing point.

This combines pv_limit_via_dyadic with cpv_exists_from_shifted_tendsto to prove CPV existence on a sub-interval containing exactly one crossing.

theorem cpv_integrand_intervalIntegrable (γ : PiecewiseC1Immersion) (z₀ : ℂ) (c d : ℝ) (hcd : c ≤ d) (h_sub : Set.Icc c d ⊆ Set.Icc γ.a γ.b) (ε : ℝ) (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ε < ‖γ.toFun t - z₀‖ then (γ.toFun t - z₀)⁻¹ * deriv γ.toFun t else 0) MeasureTheory.volume c d

The cutoff integrand for (z - z₀)⁻¹ is interval-integrable along a piecewise C¹ curve. The integrand is bounded: (γ(t) - z₀)⁻¹ is bounded by 1/ε on the region ‖γ(t) - z₀‖ > ε, and the derivative is locally bounded by continuity.

theorem cpv_exists_inv_sub (γ : PiecewiseC1Immersion) (z₀ : ℂ) (hγ_meas : Measurable γ.toFun) (h_no_endpt : γ.toFun γ.a ≠ z₀ ∧ γ.toFun γ.b ≠ z₀) (hC2 : ∀ t ∈ Set.Ioo γ.a γ.b, γ.toFun t = z₀ → ContDiffAt ℝ 2 γ.toFun t) (h_cont_deriv_cross : ∀ t ∈ Set.Ioo γ.a γ.b, γ.toFun t = z₀ → ∃ (a' : ℝ) (b' : ℝ), t ∈ Set.Ioo a' b' ∧ Set.Icc a' b' ⊆ Set.Icc γ.a γ.b ∧ ContinuousOn (deriv γ.toFun) (Set.Icc a' b')) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - z₀)⁻¹) γ.toFun γ.a γ.b z₀

CPV of (z - z₀)⁻¹ exists along a piecewise C¹ immersion.

Hypotheses:

• hγ_meas: γ is (Borel) measurable (follows from global continuity)
• h_no_endpt: γ doesn't cross z₀ at the endpoints a, b
• hC2: γ is C² at each interior crossing point
• h_cont_deriv_cross: the derivative is continuous near each crossing

The proof uses cpv_exists_on_subinterval with the cardinality of the full crossing set as the induction bound.

theorem cpv_exists_inv_sub_of_C2 (γ : PiecewiseC1Immersion) (z₀ : ℂ) (hγ_meas : Measurable γ.toFun) (h_no_endpt : γ.toFun γ.a ≠ z₀ ∧ γ.toFun γ.b ≠ z₀) (hC2 : ∀ t ∈ Set.Icc γ.a γ.b, ContDiffAt ℝ 2 γ.toFun t) (h_cont_deriv : ContinuousOn (deriv γ.toFun) (Set.Icc γ.a γ.b)) : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - z₀)⁻¹) γ.toFun γ.a γ.b z₀

CPV of (z - z₀)⁻¹ exists along a piecewise C¹ immersion, for the common case where the curve is globally C² and measurable.

This is a simplified version of the general theorem where C² regularity holds everywhere (not just at crossings), which is the typical case for smooth curves like the fundamental domain boundary.