Winding weights of planar curves

The area weight is the real part of the existing contour winding number off the trace and zero on the trace. This convention makes the weight independent of any principal-value interpretation on the trace. For a closed absolutely continuous curve it is measurable, compactly supported, and area-integrable. The integrability proof dominates the weight by the inverse-distance potential of the curve's integrable speed; the planar inverse-distance kernel is locally integrable.

noncomputable def TauCeti.Green.windingWeight (γ : ℝ → ℂ) (a b : ℝ) (z : ℂ) : ℝ

The real winding weight, set to zero on the curve trace.

Equations

• TauCeti.Green.windingWeight γ a b z = if z ∈ γ '' Set.uIcc a b then 0 else (TauCeti.Contour.windingNumber γ a b z).re

theorem TauCeti.Green.windingWeight_def (γ : ℝ → ℂ) (a b : ℝ) (z : ℂ) : windingWeight γ a b z = if z ∈ γ '' Set.uIcc a b then 0 else (Contour.windingNumber γ a b z).re

The winding weight is the existing real index off the trace, and zero on the trace.

@[simp]

theorem TauCeti.Green.windingWeight_eq_zero_of_mem {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hz : z ∈ γ '' Set.uIcc a b) : windingWeight γ a b z = 0

On the trace the area weight is zero.

@[simp]

theorem TauCeti.Green.windingWeight_eq_of_notMem {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hz : z ∉ γ '' Set.uIcc a b) : windingWeight γ a b z = (Contour.windingNumber γ a b z).re

Off the trace the area weight is the real part of the existing winding number.

@[simp]

theorem TauCeti.Green.windingWeight_const (w : ℂ) (a b : ℝ) (z : ℂ) : windingWeight (fun (x : ℝ) => w) a b z = 0

A constant curve has zero winding weight everywhere.

theorem AbsolutelyContinuousOnInterval.windingWeight_eventuallyEq_of_notMem {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hz : z ∉ γ '' Set.uIcc a b) : TauCeti.Green.windingWeight γ a b =ᶠ[nhds z] fun (x : ℂ) => TauCeti.Green.windingWeight γ a b z

The winding weight is constant on a neighborhood of any point off the trace of a closed absolutely continuous curve.

theorem AbsolutelyContinuousOnInterval.measurable_windingWeight {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : Measurable (TauCeti.Green.windingWeight γ a b)

The winding weight of an absolutely continuous curve is measurable.

theorem AbsolutelyContinuousOnInterval.exists_int_windingWeight {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (z : ℂ) : ∃ (n : ℤ), TauCeti.Green.windingWeight γ a b z = ↑n

Every value of a closed absolutely continuous curve's winding weight is an integer.

theorem AbsolutelyContinuousOnInterval.windingWeight_eq_zero_of_notMem_filledHull {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hz : z ∉ TauCeti.filledHull (γ '' Set.uIcc a b)) : TauCeti.Green.windingWeight γ a b z = 0

The winding weight vanishes outside the filled hull of the trace.

theorem AbsolutelyContinuousOnInterval.windingWeight_eq_indicator_of_index {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (n : ℤ) (hindex : ∀ z ∈ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b, TauCeti.Contour.windingNumber γ a b z = ↑n) : TauCeti.Green.windingWeight γ a b = (TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b).indicator fun (x : ℂ) => ↑n

A constant integer index throughout the bounded complementary region makes the winding weight that integer times the region's indicator.

theorem AbsolutelyContinuousOnInterval.support_windingWeight_subset {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) : Function.support (TauCeti.Green.windingWeight γ a b) ⊆ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b

The support of the winding weight lies in the intrinsic planar inside.

theorem AbsolutelyContinuousOnInterval.support_windingWeight_subset_closedBall {γ : ℝ → ℂ} {a b : ℝ} {c : ℂ} {R : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (hR : ∀ t ∈ Set.uIcc a b, γ t ∈ Metric.closedBall c R) : Function.support (TauCeti.Green.windingWeight γ a b) ⊆ Metric.closedBall c R

A ball containing a closed absolutely continuous curve also contains its winding support.

theorem AbsolutelyContinuousOnInterval.hasCompactSupport_windingWeight {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) : HasCompactSupport (TauCeti.Green.windingWeight γ a b)

The winding weight of a closed absolutely continuous curve has compact support.

theorem AbsolutelyContinuousOnInterval.integrable_windingWeight {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) : MeasureTheory.Integrable (TauCeti.Green.windingWeight γ a b) MeasureTheory.volume

The winding weight of a closed absolutely continuous planar curve is area-integrable.

theorem AbsolutelyContinuousOnInterval.tsupport_windingWeight_subset {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) (htrace : γ '' Set.uIcc a b ⊆ U) (hindex : ∀ z ∉ U, TauCeti.Contour.windingNumber γ a b z = 0) : tsupport (TauCeti.Green.windingWeight γ a b) ⊆ U

Local constancy prevents the winding support from accumulating at an excluded point away from the trace. Thus an index-vanishing domain containing the trace contains the topological support of the winding weight.

theorem AbsolutelyContinuousOnInterval.isCompact_trace_union_tsupport_windingWeight {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) : IsCompact (γ '' Set.uIcc a b ∪ tsupport (TauCeti.Green.windingWeight γ a b))

The trace and winding support of a closed AC curve have compact union.

theorem TauCeti.Green.integral_windingWeight_mul_eq_setIntegral {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} (hindex : ∀ z ∉ U, Contour.windingNumber γ a b z = 0) (R : ℂ → ℝ) : ∫ (z : ℂ), windingWeight γ a b z * R z = ∫ (z : ℂ) in U, windingWeight γ a b z * R z

Index vanishing outside a domain identifies the whole-plane weighted area integral with its restriction to that domain. This equality needs no field regularity.