Basic API for null-homologous contours

The contour-integration roadmap uses Contour.IsNullHomologous γ a b Ω as the hypothesis that a curve has zero generalized winding number about every point outside the domain Ω. This file records the elementary set-theoretic API for that predicate: monotonicity in the ambient domain, the universal and empty-domain boundary cases, intersections, unions, and replacement by another curve with the same winding numbers off the domain.

These lemmas are prerequisites for the homology Cauchy theorem and for the Hungerbühler--Wasem generalized residue theorem, where the same cycle is repeatedly viewed inside larger or smaller domains and the proof only needs the vanishing of the winding number on the complement.

Main results

• Contour.IsNullHomologous.mono — enlarge the ambient domain.
• Contour.IsNullHomologous.inter, Contour.isNullHomologous_iInter — combine null-homology hypotheses by intersecting domains.
• Contour.IsNullHomologous.union_left, Contour.IsNullHomologous.union_right — a null-homologous curve remains null-homologous after adjoining an extra part of the domain.
• Contour.isNullHomologous_const, Contour.isNullHomologous_empty_iff, Contour.isNullHomologous_univ — constant curves and the two boundary cases.
• Contour.IsNullHomologous.refl, Contour.IsNullHomologous.of_eq — a zero-length parameter interval is null-homologous in every ambient set.
• Contour.IsNullHomologous.congr_windingNumber — replace a curve by another with the same winding numbers outside the domain.

Provenance

This is routine API around the Hungerbühler--Wasem null-homology condition from the contour integration roadmap; no formal source is vendored.

@[simp]

theorem TauCeti.Contour.isNullHomologous_univ (γ : ℝ → ℂ) (a b : ℝ) : IsNullHomologous γ a b Set.univ

A curve is null-homologous in the whole plane, since there are no exterior points.

@[simp]

theorem TauCeti.Contour.isNullHomologous_const (x : ℂ) (a b : ℝ) (Ω : Set ℂ) : IsNullHomologous (fun (x_1 : ℝ) => x) a b Ω

A constant curve is null-homologous in every ambient set and on every parameter interval.

@[simp]

theorem TauCeti.Contour.isNullHomologous_empty_iff {γ : ℝ → ℂ} {a b : ℝ} : IsNullHomologous γ a b ∅ ↔ ∀ (w : ℂ), windingNumber γ a b w = 0

Null-homology in the empty set is exactly vanishing of the winding number about every point.

theorem TauCeti.Contour.IsNullHomologous.refl (γ : ℝ → ℂ) (a : ℝ) (Ω : Set ℂ) : IsNullHomologous γ a a Ω

Every zero-length parameter interval is null-homologous in every ambient set.

theorem TauCeti.Contour.IsNullHomologous.of_eq (γ : ℝ → ℂ) {a b : ℝ} (hab : a = b) (Ω : Set ℂ) : IsNullHomologous γ a b Ω

If the two endpoints are equal, the parameter interval is null-homologous in every ambient set.

theorem TauCeti.Contour.isNullHomologous_empty_of_forall_windingNumber_eq_zero {γ : ℝ → ℂ} {a b : ℝ} (h : ∀ (w : ℂ), windingNumber γ a b w = 0) : IsNullHomologous γ a b ∅

If every winding number vanishes, then the curve is null-homologous in the empty set.

theorem TauCeti.Contour.IsNullHomologous.mono {γ : ℝ → ℂ} {a b : ℝ} {Ω Ω' : Set ℂ} (h : IsNullHomologous γ a b Ω) (hΩ : Ω ⊆ Ω') : IsNullHomologous γ a b Ω'

Null-homology is monotone in the ambient domain: enlarging the domain shrinks its complement.

theorem TauCeti.Contour.IsNullHomologous.of_empty {γ : ℝ → ℂ} {a b : ℝ} {Ω : Set ℂ} (h : IsNullHomologous γ a b ∅) : IsNullHomologous γ a b Ω

A curve null-homologous in the empty set is null-homologous in every set.

theorem TauCeti.Contour.IsNullHomologous.mono_compl {γ : ℝ → ℂ} {a b : ℝ} {Ω Ω' : Set ℂ} (h : IsNullHomologous γ a b Ω) (hΩ : Ω'ᶜ ⊆ Ωᶜ) : IsNullHomologous γ a b Ω'

A complement-subset form of Contour.IsNullHomologous.mono.

theorem TauCeti.Contour.isNullHomologous_of_compl_subset {γ : ℝ → ℂ} {a b : ℝ} {Ω E : Set ℂ} (hE : Ωᶜ ⊆ E) (h : ∀ w ∈ E, windingNumber γ a b w = 0) : IsNullHomologous γ a b Ω

It suffices to prove winding-number vanishing on any set containing the complement of Ω.

theorem TauCeti.Contour.IsNullHomologous.congr_windingNumber {γ η : ℝ → ℂ} {a b c d : ℝ} {Ω : Set ℂ} (h : IsNullHomologous γ a b Ω) (hwind : ∀ w ∉ Ω, windingNumber η c d w = windingNumber γ a b w) : IsNullHomologous η c d Ω

If two curves have the same winding numbers outside Ω, null-homology transfers from one to the other. This is the replacement principle used by homotopy or decomposition arguments before the homology Cauchy theorem.

theorem TauCeti.Contour.IsNullHomologous.union_left {γ : ℝ → ℂ} {a b : ℝ} {Ω Ω' : Set ℂ} (h : IsNullHomologous γ a b Ω) : IsNullHomologous γ a b (Ω ∪ Ω')

If a curve is null-homologous in Ω, then it is null-homologous in Ω ∪ Ω'.

theorem TauCeti.Contour.IsNullHomologous.union_right {γ : ℝ → ℂ} {a b : ℝ} {Ω Ω' : Set ℂ} (h : IsNullHomologous γ a b Ω') : IsNullHomologous γ a b (Ω ∪ Ω')

If a curve is null-homologous in Ω', then it is null-homologous in Ω ∪ Ω'.

theorem TauCeti.Contour.IsNullHomologous.inter {γ : ℝ → ℂ} {a b : ℝ} {Ω Ω' : Set ℂ} (hΩ : IsNullHomologous γ a b Ω) (hΩ' : IsNullHomologous γ a b Ω') : IsNullHomologous γ a b (Ω ∩ Ω')

If a curve is null-homologous in each of two domains, it is null-homologous in their intersection.

theorem TauCeti.Contour.isNullHomologous_iInter {γ : ℝ → ℂ} {a b : ℝ} {ι : Sort u_1} {Ω : ι → Set ℂ} (h : ∀ (i : ι), IsNullHomologous γ a b (Ω i)) : IsNullHomologous γ a b (⋂ (i : ι), Ω i)

If a curve is null-homologous in every member of an indexed family, then it is null-homologous in the intersection of the family.