Flatness and Higher-Order Pole Conditions (Definition 3.2)

Flatness of curves at crossing points and conditions (A)/(B) for the generalized residue theorem with higher-order poles.

Main Definitions

• orthogonalProjectionComplex — projection of w onto direction L in C viewed as R^2
• tangentDeviation — orthogonal deviation of w from direction L
• IsFlatOfOrder — curve is flat of order n at a crossing point (Definition 3.2)
• SatisfiesConditionA — flatness condition for higher-order poles
• SatisfiesConditionB — angle/Laurent compatibility condition

Main Results

• isFlatOfOrder_one — every piecewise C^1 immersion is flat of order 1
• satisfiesConditionA_of_simple_poles — condition A automatic for simple poles
• satisfiesConditionB_of_simple_poles — condition B automatic for simple poles
• conditions_automatic_simple_poles — both conditions automatic for simple poles

Reference: Hungerbuhler-Wasem, arXiv:1808.00997v2, Definition 3.2.

Orthogonal projection in C (viewed as R^2)

noncomputable def orthogonalProjectionComplex (w L : ℂ) : ℂ

The orthogonal projection of w onto the real line spanned by L in C, where C is viewed as R^2. This computes (Re(w * conj L) / ||L||^2) * L.

Equations

• orthogonalProjectionComplex w L = ((w * (starRingEnd ℂ) L).re / Complex.normSq L) • L

noncomputable def tangentDeviation (w L : ℂ) : ℂ

The tangent deviation: the component of w orthogonal to L.

Equations

• tangentDeviation w L = w - orthogonalProjectionComplex w L

theorem orthogonalProjectionComplex_zero_left (L : ℂ) : orthogonalProjectionComplex 0 L = 0

theorem tangentDeviation_zero_left (L : ℂ) : tangentDeviation 0 L = 0

theorem tangentDeviation_zero_right (w : ℂ) : tangentDeviation w 0 = w

theorem orthogonalProjectionComplex_smul (w L : ℂ) : ∃ (c : ℝ), orthogonalProjectionComplex w L = c • L

Projection onto a nonzero direction L gives a real multiple of L.

theorem orthogonalProjectionComplex_real_smul_self (c : ℝ) (L : ℂ) (hL : L ≠ 0) : orthogonalProjectionComplex (c • L) L = c • L

Projection of a real scalar multiple of L onto L is itself.

theorem tangentDeviation_real_smul_self (c : ℝ) (L : ℂ) (hL : L ≠ 0) : tangentDeviation (c • L) L = 0

Tangent deviation of a real scalar multiple of L vanishes.

theorem tangentDeviation_add (w₁ w₂ L : ℂ) : tangentDeviation (w₁ + w₂) L = tangentDeviation w₁ L + tangentDeviation w₂ L

Tangent deviation is additive in the first argument.

theorem norm_tangentDeviation_le (w L : ℂ) (hL : L ≠ 0) : ‖tangentDeviation w L‖ ≤ 2 * ‖w‖

Norm bound: ‖tangentDeviation w L‖ ≤ 2 * ‖w‖ for L ≠ 0.

Flatness of order n (Definition 3.2)

A piecewise C^1 curve gamma is flat of order n at a parameter t_0 if the orthogonal deviation from the tangent line at gamma(t_0) is o(||gamma(t) - gamma(t_0)||^n) as t -> t_0, where the tangent line is determined by the one-sided derivative limits.

structure IsFlatOfOrder (γ : ℝ → ℂ) (t₀ : ℝ) (n : ℕ) : Prop

A curve gamma is flat of order n at parameter t_0 if:

• From the right: the deviation from the right tangent is o(||gamma(t) - gamma(t_0)||^n)
• From the left: the deviation from the left tangent is o(||gamma(t) - gamma(t_0)||^n)

This captures Definition 3.2 from Hungerbuhler-Wasem: the curve stays within o(|Gamma(x) - z_1|^n) of the tangent lines at the crossing point z_1.

• right_flat (L : ℂ) : L ≠ 0 → Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L) → (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhdsWithin t₀ (Set.Ioi t₀)] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ n

  From the right: deviation from right tangent direction is o(||gamma(t) - gamma(t_0)||^n).

• left_flat (L : ℂ) : L ≠ 0 → Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L) → (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhdsWithin t₀ (Set.Iio t₀)] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ n

  From the left: deviation from left tangent direction is o(||gamma(t) - gamma(t_0)||^n).

theorem IsFlatOfOrder.of_le {γ : ℝ → ℂ} {t₀ : ℝ} {m n : ℕ} (h : IsFlatOfOrder γ t₀ m) (hmn : n ≤ m) (hγ_cont : ContinuousAt γ t₀) : IsFlatOfOrder γ t₀ n

Flatness of order m implies flatness of order n for n <= m. The key point is that o(||w||^m) implies o(||w||^n) when n <= m and ||w|| -> 0.

Flatness of order 1 is automatic

Every piecewise C^1 immersion is flat of order 1 at every point. This is because the derivative approximation gamma(t) - gamma(t_0) ~ gamma'(t_0)(t - t_0) ensures the curve direction is asymptotically aligned with the tangent.

theorem tangentDeviation_isLittleO_of_hasDerivAt (γ : ℝ → ℂ) (t₀ : ℝ) (L : ℂ) (hL : L ≠ 0) (hγ : HasDerivAt γ L t₀) : (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhds t₀] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ 1

Key lemma: if gamma has derivative L at t_0, then the tangent deviation of gamma(t) - gamma(t_0) from L is o(||gamma(t) - gamma(t_0)||) as t -> t_0. This is the essential content of flatness of order 1.

The argument: gamma(t) - gamma(t_0) = (t - t_0) * L + o(t - t_0), so the deviation from L is exactly the remainder term, which is o(t - t_0). Meanwhile ||gamma(t) - gamma(t_0)|| >= (||L||/2)|t - t_0| eventually, giving o(t - t_0) = o(||gamma(t) - gamma(t_0)||).

theorem tangentDeviation_isLittleO_right (γ : ℝ → ℂ) (t₀ : ℝ) (L : ℂ) (hL : L ≠ 0) (hγ_right : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L)) (hγ_cont : ContinuousAt γ t₀) (hγ_diff : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), DifferentiableAt ℝ γ t) : (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhdsWithin t₀ (Set.Ioi t₀)] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ 1

Tangent deviation from right derivative limit is o(||gamma(t) - gamma(t_0)||) as t -> t_0+. This is the right-sided version needed for flatness of order 1.

theorem tangentDeviation_isLittleO_left (γ : ℝ → ℂ) (t₀ : ℝ) (L : ℂ) (hL : L ≠ 0) (hγ_left : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L)) (hγ_cont : ContinuousAt γ t₀) (hγ_diff : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), DifferentiableAt ℝ γ t) : (fun (t : ℝ) => ‖tangentDeviation (γ t - γ t₀) L‖) =o[nhdsWithin t₀ (Set.Iio t₀)] fun (t : ℝ) => ‖γ t - γ t₀‖ ^ 1

Tangent deviation from left derivative limit is o(||gamma(t) - gamma(t_0)||) as t -> t_0-. This is the left-sided version needed for flatness of order 1.

theorem isFlatOfOrder_one (γ : PiecewiseC1Immersion) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) : IsFlatOfOrder γ.toFun t₀ 1

Every piecewise C^1 immersion is flat of order 1 at any interior point. This is because the first-order Taylor approximation gamma(t) - gamma(t_0) ~ L*(t-t_0) lies exactly on the tangent line, so the deviation is the remainder o(t-t_0) = o(||gamma(t)-gamma(t_0)||).

Pole order

noncomputable def poleOrderAt (f : ℂ → ℂ) (x : ℂ) : ℕ

The pole order of a meromorphic function at a point, as a natural number. Returns 0 if f is analytic at x (including the case where f is identically zero near x). Returns n if f has a pole of order n (i.e., meromorphicOrderAt f x = -n).

Equations

• poleOrderAt f x = (-(meromorphicOrderAt f x).untop₀).toNat

Condition (A): Flatness condition for higher-order poles

def SatisfiesConditionA (γ : PiecewiseC1Immersion) (S0 : Finset ℂ) : Prop

Condition (A) from Hungerbuhler-Wasem: if z_0 is a pole of order n of f on the curve, then the curve is flat of order n at z_0.

More precisely: for each singular point s in S_0 and each parameter t_0 where gamma(t_0) = s, if f has a pole of order n at s, then gamma must be flat of order n at t_0.

For the current formalization, which focuses on simple poles, this is stated using HasSimplePoleAt. The condition is that the curve is flat of order 1 at each crossing, which is automatic (see isFlatOfOrder_one).

Equations

• SatisfiesConditionA γ S0 = ∀ s ∈ S0, ∀ t₀ ∈ Set.Icc γ.a γ.b, γ.toFun t₀ = s → t₀ ∈ Set.Ioo γ.a γ.b → IsFlatOfOrder γ.toFun t₀ 1

def SatisfiesConditionA' (γ : PiecewiseC1Immersion) (S0 : Finset ℂ) (poleOrder : ℂ → ℕ) : Prop

Condition (A) for a specific pole order function. Given a function assigning pole orders to singular points, the curve must be flat of the corresponding order at each crossing.

Equations

• SatisfiesConditionA' γ S0 poleOrder = ∀ s ∈ S0, ∀ t₀ ∈ Set.Icc γ.a γ.b, γ.toFun t₀ = s → t₀ ∈ Set.Ioo γ.a γ.b → IsFlatOfOrder γ.toFun t₀ (poleOrder s)

Condition (B): Angle/Laurent compatibility

structure SatisfiesConditionB (γ : PiecewiseC1Immersion) (f : ℂ → ℂ) (S0 : Finset ℂ) : Prop

Condition (B) from Hungerbuhler-Wasem (Theorem 3.3): at each crossing point, the angle α is a rational multiple of π, and the Laurent coefficients of f satisfy angle compatibility.

Concretely: if f has a pole of order N at s, then near s we can write f(z) = Res(f,s)/(z-s) + Σ_{k=2}^{N} cₖ/(z-s)^k + g(z) where g is analytic. Condition (B) requires that for each k ≥ 2 with cₖ ≠ 0, the angle α at the crossing satisfies (k-1) · α ∈ 2πℤ. This ensures PV ∮ dz/(z-s)^k = 0 on the model sector curve (equation 3.4 in the paper).

• angle_rational (s : ℂ) : s ∈ S0 → ∀ t₀ ∈ Set.Icc γ.a γ.b, γ.toFun t₀ = s → ∀ (ht₀_Ioo : t₀ ∈ Set.Ioo γ.a γ.b), ∃ (p : ℕ) (q : ℕ), q ≠ 0 ∧ p.Coprime q ∧ angleAtCrossing γ t₀ ht₀_Ioo = ↑p * Real.pi / ↑q

  The angle at each crossing point on the curve is a rational multiple of π.

• laurent_compatible (s : ℂ) : s ∈ S0 → ∀ t₀ ∈ Set.Icc γ.a γ.b, γ.toFun t₀ = s → ∀ (ht₀_Ioo : t₀ ∈ Set.Ioo γ.a γ.b), ∃ (N : ℕ) (a : Fin N → ℂ) (g : ℂ → ℂ), AnalyticAt ℂ g s ∧ (∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, f z = g z + ∑ k : Fin N, a k / (z - s) ^ (↑k + 1)) ∧ ∀ (k : Fin N), a k ≠ 0 → ↑k ≥ 1 → ∃ (m : ℤ), ↑↑k * angleAtCrossing γ t₀ ht₀_Ioo = ↑m * (2 * Real.pi)

  Laurent coefficient compatibility: there exists a Laurent decomposition of f near each pole s into f(z) = Σ_{k=1}^{N} aₖ/(z-s)^k + g(z) where g is analytic, and each nonzero coefficient aₖ with k ≥ 2 satisfies (k-1)·α ∈ 2πℤ. This ensures PV ∮ aₖ/(z-s)^k dz = 0 on the model sector.

  For simple poles (N = 0 higher-order terms), this is vacuously true.

Conditions are automatic for simple poles

For simple poles (order 1), both conditions are automatically satisfied:

• (A): Simple poles have order 1, and every piecewise C^1 curve is flat of order 1 (proved above as isFlatOfOrder_one).

• (B): A simple pole has Laurent series f(z) = c_1/(z-z_0) + g(z), so the only singular term is k = 1 (the residue term). The condition "q does not divide (k-1) for k != 1" is vacuously true since there are no other singular terms. The angle rationality is trivially satisfied.

theorem satisfiesConditionA_of_simple_poles (γ : PiecewiseC1Immersion) (f : ℂ → ℂ) (S0 : Finset ℂ) (_hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) : SatisfiesConditionA γ S0

Condition (A) is automatically satisfied when all poles are simple, because every piecewise C^1 curve is flat of order 1.

theorem satisfiesConditionB_of_simple_poles (γ : PiecewiseC1Immersion) (f : ℂ → ℂ) (S0 : Finset ℂ) (_hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hAngles : ∀ s ∈ S0, ∀ t₀ ∈ Set.Icc γ.a γ.b, γ.toFun t₀ = s → ∀ (ht₀_Ioo : t₀ ∈ Set.Ioo γ.a γ.b), t₀ ∈ γ.partition → ∃ (p : ℕ) (q : ℕ), q ≠ 0 ∧ p.Coprime q ∧ angleAtCrossing γ t₀ ht₀_Ioo = ↑p * Real.pi / ↑q) : SatisfiesConditionB γ f S0

Condition (B) for simple poles requires angle rationality at corner crossings as an explicit hypothesis. The Laurent coefficient condition is vacuously true (the only singular term is k = 1), so any q works; but the angle itself must be expressible as pπ/q. At smooth crossings the angle is π = 1·π/1, so this is automatic. At corner crossings, the angle depends on the curve geometry and is not guaranteed to be rational without additional assumptions.

Note: For simple poles, the main theorem (Proposition 2.2 / generalizedResidueTheorem') does NOT require condition (B). This lemma is only needed when using the higher-order theorem (Theorem 3.3) with simple poles.

theorem conditions_automatic_simple_poles (γ : PiecewiseC1Immersion) (f : ℂ → ℂ) (S0 : Finset ℂ) (hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hAngles : ∀ s ∈ S0, ∀ t₀ ∈ Set.Icc γ.a γ.b, γ.toFun t₀ = s → ∀ (ht₀_Ioo : t₀ ∈ Set.Ioo γ.a γ.b), t₀ ∈ γ.partition → ∃ (p : ℕ) (q : ℕ), q ≠ 0 ∧ p.Coprime q ∧ angleAtCrossing γ t₀ ht₀_Ioo = ↑p * Real.pi / ↑q) : SatisfiesConditionA γ S0 ∧ SatisfiesConditionB γ f S0

Both conditions (A) and (B) are satisfied for simple poles, provided corner crossing angles are rational multiples of π. Condition (A) is fully automatic; condition (B) requires the angle hypothesis only at corners.

Note: For simple poles, one should typically use generalizedResidueTheorem' (Proposition 2.2) which requires neither condition.