Winding normalization from oriented convex geometry

For a consistently oriented point c of a smooth strictly convex carrier, the logarithmic derivative

gamma'(t) / (gamma(t) - c)

has strictly positive imaginary part. Its interval integral is therefore a strictly increasing argument lift. Solving the associated exponential ODE and using periodicity shows that the lift changes by a positive natural multiple of 2 * pi over one period.

There cannot be two turns: the intermediate value theorem would then give a second boundary point on the same positive ray from c as the initial one. Convexity puts the nearer of two such frontier points in the open carrier, unless the points coincide; fundamental-interval injectivity excludes that last possibility. Thus the winding is exactly one.

Main declarations

• crouzeixScalarCauchyKernel_eq_one_of_oriented_carrier_point -- oriented convex geometry normalizes the kernel at the selected carrier point;
• crouzeixScalarCauchyKernel_eq_one_of_oriented_carrier -- the normalization propagates throughout the carrier.

theorem crouzeixScalarCauchyKernel_eq_one_of_oriented_carrier_point (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) : crouzeixScalarCauchyKernel Omega c = 1

A consistently oriented carrier point has normalized scalar winding one. The proof obtains the total argument change from the logarithmic-derivative ODE and uses convexity to exclude every positive integer other than one.

theorem crouzeixScalarCauchyKernel_eq_one_of_oriented_carrier (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (z : ℂ) : z ∈ Omega.carrier → crouzeixScalarCauchyKernel Omega z = 1

Consistent orientation at one carrier point forces winding normalization at every point of the strictly convex carrier.