Finite weighted winding supports #
Finite integer-weighted families of closed absolutely continuous curves have integrable, compactly supported total winding weight. If the total index vanishes outside a field domain containing every trace, the total weight's topological support lies in that domain. Individual indices may cancel there.
theorem
TauCeti.Green.integrable_sum_windingWeight
{ι : Type u_1}
{s : Finset ι}
{γ : ι → ℝ → ℂ}
{a b : ι → ℝ}
{w : ι → ℤ}
(hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i))
(hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i))
:
MeasureTheory.Integrable (fun (z : ℂ) => ∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) MeasureTheory.volume
A finite weighted sum of closed absolutely continuous winding weights is integrable.
theorem
TauCeti.Green.hasCompactSupport_sum_windingWeight
{ι : Type u_1}
{s : Finset ι}
{γ : ι → ℝ → ℂ}
{a b : ι → ℝ}
{w : ι → ℤ}
(hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i))
(hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i))
:
HasCompactSupport fun (z : ℂ) => ∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z
Finite weighted winding families have compact support without a bounded-index assumption.
theorem
TauCeti.Green.tsupport_sum_windingWeight_subset
{ι : Type u_1}
{s : Finset ι}
{γ : ι → ℝ → ℂ}
{a b : ι → ℝ}
{w : ι → ℤ}
{U : Set ℂ}
(hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i))
(hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i))
(htrace : ∀ i ∈ s, γ i '' Set.uIcc (a i) (b i) ⊆ U)
(hindex : ∀ z ∉ U, ∑ i ∈ s, ↑(w i) * Contour.windingNumber (γ i) (a i) (b i) z = 0)
:
(tsupport fun (z : ℂ) => ∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z) ⊆ U
Vanishing of the total index outside a domain suffices to localize the total winding weight. No vanishing condition is imposed on the individual curves.
theorem
TauCeti.Green.isCompact_traces_union_tsupport_sum_windingWeight
{ι : Type u_1}
{s : Finset ι}
{γ : ι → ℝ → ℂ}
{a b : ι → ℝ}
{w : ι → ℤ}
(hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i))
(hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i))
:
Finitely many closed AC traces and their total weighted winding support have compact union.