L¹ bounds for winding weights

The winding weight of a curve contained in a disk has L¹ norm bounded by twice the radius multiplied by its total variation, equal to its integral speed. Differences of winding weights are controlled by the associated compactly truncated Cauchy potentials.

theorem TauCeti.Green.integral_norm_windingWeight_sub_le_cauchyPotential {γ δ : ℝ → ℂ} {a b R : ℝ} {c : ℂ} (hab : a ≤ b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hδ : AbsolutelyContinuousOnInterval δ a b) (hγclosed : γ a = γ b) (hδclosed : δ a = δ b) (hγR : ∀ t ∈ Set.uIcc a b, γ t ∈ Metric.closedBall c R) (hδR : ∀ t ∈ Set.uIcc a b, δ t ∈ Metric.closedBall c R) : ∫ (z : ℂ), ‖windingWeight δ a b z - windingWeight γ a b z‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * ∫ (z : ℂ), ‖(∫ (t : ℝ) in Set.Ioc a b, truncatedCauchyKernel (2 * R) (z - δ t) * deriv δ t) - ∫ (t : ℝ) in Set.Ioc a b, truncatedCauchyKernel (2 * R) (z - γ t) * deriv γ t‖

A winding-weight difference is controlled in L¹ by the truncated Cauchy potentials.

theorem TauCeti.Green.integral_abs_windingWeight_le {γ : ℝ → ℂ} {a b R : ℝ} {c : ℂ} (hab : a ≤ b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hR : ∀ t ∈ Set.uIcc a b, γ t ∈ Metric.closedBall c R) : ∫ (z : ℂ), |windingWeight γ a b z| ≤ 2 * R * (eVariationOn γ (Set.uIcc a b)).toReal

A closed absolutely continuous curve in a disk of radius R has winding-weight L¹ norm at most 2R times its total variation.