Modular Forms — Hungerbühler–Wasem & Valence Formula in Lean

1. Closed piecewise-C¹ immersions and null-homology🔗

This chapter introduces the curve types underlying the Hungerbühler–Wasem residue theorem. The basic carrier is the closed piecewise-C^{1} immersion: a closed curve in \mathbb{C} that is C^{1} on each of finitely many closed sub-intervals between partition points, with nowhere-vanishing derivative. The second concept, null-homology in an open set U, is the topological condition required to apply the residue theorem along such a curve.

Definition1.1
uses 0
Used by 9
Reverse dependency previews
Preview
Definition 1.2
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let x \in E be a point of a real normed vector space E. A closed piecewise-C^{1} immersion based at x is the following data:

  • a continuous path \gamma : [0,1] \to E with \gamma(0) = \gamma(1) = x;

  • a finite closed partition 0 = a_0 < a_1 < \cdots < a_n = 1 of [0,1];

  • on every closed sub-interval [a_k, a_{k+1}] between consecutive partition members, the (extended) path \gamma : [a_k, a_{k+1}] \to E is of class C^{1} and its one-sided within-derivative is nowhere zero: \dot{\gamma}|_{[a_k, a_{k+1}]}(t) \ne 0 \quad \text{for every } t \in [a_k, a_{k+1}].

This is the paper-faithful definition from Hungerbühler–Wasem 2018, page 3. The non-vanishing-on-each-closed-piece convention forces a well-defined right/left limit of \dot{\gamma} at every partition point and, in particular, two non-zero tangent vectors at each corner of \gamma.

Lean code for Definition1.1●1 definition
  • structure(extends 3, 17 fields)defined in LeanModularForms/ForMathlib/PaperPwC1Immersion.lean
    complete
    structure ClosedPwC1Immersion.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (x : E) : Type u_1
    structure ClosedPwC1Immersion.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  (x : E) : Type u_1
    A **closed piecewise `C¹` immersion** in the sense of Hungerbühler–Wasem
(arXiv:1808.00997v2, page 3): a closed piecewise `C¹` curve whose derivative
is non-vanishing on every closed sub-interval between consecutive partition
points.

    Extends

    • ClosedPwC1Curve x

    Fields

    toFun : ℝ → E
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    source : self.toFun 0 = x
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    target : self.toFun 1 = x
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    continuous_toFun : ContinuousOn self.toFun (Set.Icc 0 1)
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    partition : Finset ℝ
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    partition_subset : ↑self.partition ⊆ Set.Ioo 0 1
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    differentiable_off : ∀ t ∈ Set.Ioo 0 1, t ∉ self.partition → DifferentiableAt ℝ self.toFun t
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    deriv_continuous_off : ∀ t ∈ Set.Ioo 0 1, t ∉ self.partition → ContinuousAt (deriv self.toFun) t
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    3. PiecewiseC1PathOn
    toPath : Path x x
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    toPath_extend_eq_toFun : ∀ t ∈ Set.Icc 0 1, self.toPath.extend t = self.toFun t
    Inherited from
    1. ClosedPwC1Curve
    2. PiecewiseC1Path
    closedPartition : Finset ℝ
    Inherited from
    1. ClosedPwC1Curve
    zero_mem_closedPartition : 0 ∈ self.closedPartition
    Inherited from
    1. ClosedPwC1Curve
    one_mem_closedPartition : 1 ∈ self.closedPartition
    Inherited from
    1. ClosedPwC1Curve
    closedPartition_subset : ↑self.closedPartition ⊆ Set.Icc 0 1
    Inherited from
    1. ClosedPwC1Curve
    closedPartition_eq : self.closedPartition = insert 0 (insert 1 self.partition)
    Inherited from
    1. ClosedPwC1Curve
    contDiffOn_pieces : ∀ (a b : ℝ), self.closedPartition.IsConsecutive a b → ContDiffOn ℝ 1 (⇑self.toPath.extend) (Set.Icc a b)
    Inherited from
    1. ClosedPwC1Curve
    derivWithin_ne_zero_pieces : ∀ (a b : ℝ),
  self.closedPartition.IsConsecutive a b → ∀ t ∈ Set.Icc a b, derivWithin (⇑self.toPath.extend) (Set.Icc a b) t ≠ 0
    On every closed sub-interval between consecutive closed-partition members, the
*within*-derivative of the extended path is non-zero — i.e. `Λ̇|_{[aₖ,aₖ₊₁]} ≠ 0`
in the paper. We use `derivWithin _ (Icc a b)` rather than the global `deriv`
because at corner partition points the global `deriv` is `0` by mathlib
convention (the function is not differentiable there), which would falsely
contradict non-vanishing.
Definition1.2
uses 1
Used by 4
Reverse dependency previews
Preview
Theorem 5.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Let U \subseteq \mathbb{C} be an open set, x \in \mathbb{C}, and \gamma a closed piecewise-C^{1} immersion based at x in the sense of Definition 1.1. We say that \gamma is null-homologous in U when both

  • the image of \gamma lies in U, that is \gamma(t) \in U for every t \in [0,1], and

  • for every point z \in \mathbb{C} \setminus U, the generalised winding number \operatorname{gWN}(\gamma, z) (see Definition 3.1) is zero.

Equivalently, \gamma has image in U and winds zero times around every point of the complement.

Definition 1.1

Lean code for Definition1.2●1 definition
  • structure(2 fields)defined in LeanModularForms/ForMathlib/NullHomologous.lean
    complete
    structure IsNullHomologous {x : ℂ} (γ : PwC1Immersion x x) (U : Set ℂ) : Prop
    structure IsNullHomologous {x : ℂ}
  (γ : PwC1Immersion x x) (U : Set ℂ) :
  Prop
    A closed piecewise C^1 immersion `gamma` is null-homologous in an open set `U` if:
1. Its image lies in `U`.
2. Its winding number around every point outside `U` is zero.

Closedness is encoded by the type: `PwC1Immersion x x` has the same start and
end point.

    Fields

    image_subset : ∀ t ∈ Set.Icc 0 1, γ.extendedPath t ∈ U
    The image of `gamma` lies in `U`. 
    winding_zero : ∀ z ∉ U, generalizedWindingNumber γ.toPiecewiseC1Path z = 0
    The generalized winding number around every point outside `U` is zero.