L¹ convergence of winding weights #
Uniform convergence of closed absolutely continuous curves, together with L¹ convergence of
their derivatives, gives global L¹ convergence of their winding weights. The estimate uses
translation continuity of a compactly truncated complex reciprocal kernel.
theorem
TauCeti.Green.tendsto_integral_abs_windingWeight_sub
{γ : ℝ → ℂ}
{a b : ℝ}
{γn : ℕ → ℝ → ℂ}
(hab : a ≤ b)
(hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b)
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hγnclosed : ∀ (n : ℕ), γn n a = γn n b)
(hγclosed : γ a = γ b)
(hconv : TendstoUniformlyOn γn γ Filter.atTop (Set.Icc a b))
(hderiv : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, ‖deriv (γn n) t - deriv γ t‖) Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), |windingWeight (γn n) a b z - windingWeight γ a b z|) Filter.atTop (nhds 0)
Uniform convergence of closed absolutely continuous curves and L¹ convergence of their
derivatives imply global L¹ convergence of their winding weights.
theorem
TauCeti.Green.tendsto_integral_abs_sum_windingWeight_sub
{ι : Type u_1}
{s : Finset ι}
{γ : ι → ℝ → ℂ}
{γn : ℕ → ι → ℝ → ℂ}
{a b : ι → ℝ}
{w : ι → ℤ}
(hab : ∀ i ∈ s, a i ≤ b i)
(hγ : ∀ i ∈ s, AbsolutelyContinuousOnInterval (γ i) (a i) (b i))
(hγn : ∀ (n : ℕ), ∀ i ∈ s, AbsolutelyContinuousOnInterval (γn n i) (a i) (b i))
(hclosed : ∀ i ∈ s, γ i (a i) = γ i (b i))
(hclosedn : ∀ (n : ℕ), ∀ i ∈ s, γn n i (a i) = γn n i (b i))
(hconv : ∀ i ∈ s, TendstoUniformlyOn (fun (n : ℕ) => γn n i) (γ i) Filter.atTop (Set.Icc (a i) (b i)))
(hdconv :
∀ i ∈ s,
Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a i..b i, ‖deriv (γn n i) t - deriv (γ i) t‖) Filter.atTop (nhds 0))
:
Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : ℂ), |∑ i ∈ s, ↑(w i) * windingWeight (γn n i) (a i) (b i) z - ∑ i ∈ s, ↑(w i) * windingWeight (γ i) (a i) (b i) z|)
Filter.atTop (nhds 0)
Per-curve uniform and derivative L¹ convergence imply L¹ convergence of the actual total
real winding weight. No uniform bound on the indices is assumed.