A decay bound for ∫ (γ - w)⁻¹ · g when w is far from the curve #
For a curve γ : ℝ → ℂ with ‖γ t‖ ≤ R on the integrating interval and a point w with
R < ‖w‖, the integral ∫ t in a..b, (γ t - w)⁻¹ * g t of an interval-integrable weight g is
bounded by (∫ ‖g‖) / (‖w‖ - R): the distance lower bound ‖w‖ - R ≤ ‖γ t - w‖ gives
‖(γ t - w)⁻¹‖ ≤ (‖w‖ - R)⁻¹ pointwise, so the estimate reduces to the L¹ norm of g. This is
the common decay estimate behind the vanishing at infinity of both the generalized winding number
(weight g = deriv γ) and Dixon's dixonH2 (weight g = f (γ ·) * deriv γ); using the L¹ norm
rather than a uniform bound on g keeps it applicable to raw curves whose derivative is only
interval-integrable.
Main results #
TauCeti.Contour.norm_integral_inv_sub_mul_le— the(∫ ‖g‖) / (‖w‖ - R)decay bound.
Provenance #
Factored from the far-field estimates in the AINTLIB LeanModularForms development —
contourIntegral_inv_norm_le_of_far in NullHomologous.lean (the winding case, weight deriv γ)
and dixonH2_norm_le in DixonTheorem.lean (the Dixon case) — restated for a raw γ : ℝ → ℂ on an
oriented interval with an arbitrary interval-integrable weight g, and bounding by the L¹ norm of
g rather than a Lipschitz or uniform bound.
Decay bound for a Cauchy-type integral far from the curve. If ‖γ t‖ ≤ R on Ι a b,
g is interval-integrable, and R < ‖w‖, then
‖∫ t in a..b, (γ t - w)⁻¹ * g t‖ ≤ (∫ t in Ι a b, ‖g t‖) / (‖w‖ - R). The distance lower bound
‖w‖ - R ≤ ‖γ t - w‖ makes ‖(γ t - w)⁻¹‖ ≤ (‖w‖ - R)⁻¹ pointwise, and the weight contributes its
L¹ norm. Only the bound on the half-open interval Ι a b matters; the endpoints do not affect the
integral.