4. Paper conditions (A') and (B)🔗

The Hungerbühler–Wasem generalised residue theorem requires two hypotheses on the geometry of the curve at crossings. Condition (A') controls the flatness of the curve transverse to its tangent at each crossing; condition (B) controls the relationship between the crossing angle and the Laurent coefficients of f at the corresponding pole.

Definition4.1

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 5.1

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Let \gamma be a piecewise-C^{1} immersion based at x, let S_0 \subseteq \mathbb{C} be a finite set, and let \operatorname{poleOrder} : \mathbb{C} \to \mathbb{N} assign a pole order to each candidate singular point. Following Hungerbühler–Wasem 2018, the immersion \gamma is said to satisfy condition (A') (relative to S_0 and \operatorname{poleOrder}) when: for every s \in S_0 and every interior parameter t_0 \in (0,1) at which \gamma(t_0) = s, the curve \gamma is flat of order \operatorname{poleOrder}(s) at t_0. That is, on each side of t_0 the deviation of \gamma from its tangent line at \gamma(t_0) is o(\|\gamma(t) - \gamma(t_0)\|^{\operatorname{poleOrder}(s)}).

Flatness of order one is automatic for a piecewise-C^{1} immersion at any interior point. Higher-order flatness is a genuine hypothesis controlling how rapidly \gamma deviates from its tangent line at a higher-order pole.

Definition 1.1

Lean code for Definition4.1●1 definition

defdefined in LeanModularForms/ForMathlib/FlatnessConditions.lean

complete

def SatisfiesConditionA' {x y : ℂ} (γ : PwC1Immersion x y) (_f : ℂ → ℂ)
  (S0 : Finset ℂ) (poleOrder : ℂ → ℕ) : Prop

def SatisfiesConditionA' {x y : ℂ}
  (γ : PwC1Immersion x y) (_f : ℂ → ℂ)
  (S0 : Finset ℂ) (poleOrder : ℂ → ℕ) :
  Prop

**Condition (A')** from Hungerbuhler-Wasem: for each singular point `s` in `S₀`
and each parameter `t₀` where `γ(t₀) = s`, the curve must be flat of order
`poleOrder s` at `t₀`.

Definition4.2

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 5.1

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Let \gamma be a piecewise-C^{1} immersion based at x, let f : \mathbb{C} \to \mathbb{C}, and let S_0 \subseteq \mathbb{C} be a finite set. Following Hungerbühler–Wasem 2018, Theorem 3.3, (\gamma, f) satisfies condition (B) (relative to S_0) when, for every s \in S_0 and every interior parameter t_0 \in (0,1) with \gamma(t_0) = s, both of the following hold.

Rational angle. The crossing angle \alpha = \operatorname{angleAtCrossing}(\gamma, t_0) is a rational multiple of \pi: there exist coprime naturals p, q with q \ne 0 and \alpha = p\pi/q.
Laurent compatibility. There exist N \in \mathbb{N}, complex coefficients a_0, \ldots, a_{N-1}, and a function g analytic at s such that f(z) = g(z) + \sum_{k=0}^{N-1} \frac{a_k}{(z - s)^{k+1}} \quad \text{for } z \text{ near } s,\, z \ne s, and, for every k \ge 1 with a_k \ne 0, the product k\alpha is an integer multiple of 2\pi: k \alpha \in 2\pi \mathbb{Z}.

Geometrically, condition (B) says that the higher-order Laurent data of f at s is compatible with the angle at which \gamma passes through s, in the precise sense required for the sector-cancellation identity (Hungerbühler–Wasem 2018, equation 3.4) to apply.

Definition 1.1

Lean code for Definition4.2●1 definition

structure(2 fields)defined in LeanModularForms/ForMathlib/FlatnessConditions.lean

complete

structure SatisfiesConditionB {x y : ℂ} (γ : PwC1Immersion x y) (f : ℂ → ℂ)
  (S0 : Finset ℂ) : Prop

structure SatisfiesConditionB {x y : ℂ}
  (γ : PwC1Immersion x y) (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.

For simple poles, this is vacuously satisfied for the Laurent part.

Fields

angle_rational : ∀ s ∈ S0,
  ∀ t₀ ∈ Set.Icc 0 1,
    γ.extendedPath t₀ = s →
      ∀ (ht₀ : t₀ ∈ Set.Ioo 0 1), ∃ p q, q ≠ 0 ∧ p.Coprime q ∧ angleAtCrossing γ t₀ ht₀ = ↑p * Real.pi / ↑q

The angle at each crossing is a rational multiple of `π`.

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

Laurent coefficient compatibility: there is a Laurent decomposition
`f(z) = g(z) + Σ_k a_k / (z - s)^(k+1)` where `g` is analytic, and each
nonzero coefficient `a_k` with `k ≥ 1` satisfies `k · α ∈ 2πℤ`.