The real winding integrand

This file defines the pointwise real winding integrand and records its coordinate formula, invariance under simultaneous nonzero complex scaling, velocity negation, vanishing at the origin, and a crude bound away from the origin.

Provenance

The pointwise imaginary-part decomposition is migrated and cleaned from the AINTLIB LeanModularForms generalized-winding-number development.

noncomputable def TauCeti.Contour.realWindingIntegrand (z v : ℂ) : ℝ

The real winding integrand (x ẏ - y ẋ) / (x² + y²) for a position z = x + iy and velocity v = ẋ + iẏ. It is defined as the imaginary part (z⁻¹ * v).im of the complex winding integrand; in particular it is 0 at z = 0. Its relation to the complex integrand is realWindingIntegrand_def and its coordinate form is realWindingIntegrand_eq_div.

Equations

• TauCeti.Contour.realWindingIntegrand z v = (z⁻¹ * v).im

theorem TauCeti.Contour.realWindingIntegrand_def (z v : ℂ) : realWindingIntegrand z v = (z⁻¹ * v).im

The real winding integrand is the imaginary part of the complex winding integrand z⁻¹ * v. This is a convenient public rewrite lemma relating the real integrand to the complex index integrand (γ - w)⁻¹ * γ'.

@[simp]

theorem TauCeti.Contour.realWindingIntegrand_eq_div (z v : ℂ) : realWindingIntegrand z v = (z.re * v.im - z.im * v.re) / Complex.normSq z

The coordinate formula for the real winding integrand.

theorem TauCeti.Contour.realWindingIntegrand_mul_mul {c : ℂ} (hc : c ≠ 0) (z v : ℂ) : realWindingIntegrand (c * z) (c * v) = realWindingIntegrand z v

Scaling position and velocity by the same nonzero complex parameter leaves the real winding integrand unchanged: it is the imaginary part of (c * z)⁻¹ * (c * v) = z⁻¹ * v, where the two factors of c cancel in ℂ.

theorem TauCeti.Contour.realWindingIntegrand_neg_right (z v : ℂ) : realWindingIntegrand z (-v) = -realWindingIntegrand z v

Negating the velocity while keeping the position fixed negates the real winding integrand: it is the imaginary part of z⁻¹ * (-v) = -(z⁻¹ * v).

theorem TauCeti.Contour.abs_realWindingIntegrand_le_div_norm (z v : ℂ) : |realWindingIntegrand z v| ≤ ‖v‖ / ‖z‖

A crude bound on the real winding integrand. realWindingIntegrand z v = (z⁻¹ * v).im, whose absolute value is at most ‖z⁻¹ * v‖ = ‖v‖ / ‖z‖ -- including at z = 0, where both sides vanish (simp [realWindingIntegrand_eq_div], div_zero).

theorem TauCeti.Contour.abs_realWindingIntegrand_le_div_of_le_norm {z v : ℂ} {m : ℝ} (hm : 0 < m) (hz : m ≤ ‖z‖) : |realWindingIntegrand z v| ≤ ‖v‖ / m

The crude bound above, weakened to a uniform denominator m ≤ ‖z‖ away from the singularity.