Norm bound and decay at infinity of Dixon's dixonH2

For w outside a ball containing the curve, Dixon's Cauchy-type integral dixonH2 f γ a b w = ∫ t in a..b, f (γ t) / (γ t - w) * deriv γ t is small and tends to 0 as ‖w‖ → ∞. The distance lower bound ‖w‖ - R ≤ ‖γ t - w‖ (for ‖γ‖ ≤ R < ‖w‖) controls the Cauchy kernel; the numerator f (γ ·) * deriv γ is then bounded either uniformly or in L¹:

• with a uniform bound M on the integrand, ‖dixonH2 f γ a b w‖ ≤ M / (‖w‖ - R) · |b - a|;
• using only interval-integrability of the weight (rewrite the integrand as (γ t - w)⁻¹ * (f (γ t) * deriv γ t)), ‖dixonH2 f γ a b w‖ ≤ (∫ ‖f (γ ·) * deriv γ‖) / (‖w‖ - R).

The two hypotheses are incomparable — the uniform bound needs no integrability, the L¹ bound needs no uniform bound — so both are kept. The L¹ form is what applies to raw curves whose derivative is only interval-integrable.

Main results

• TauCeti.Contour.dixonH2_norm_le / dixonH2_tendsto_zero — the uniform-bound norm estimate and its decay at infinity.
• TauCeti.Contour.dixonH2_norm_le_of_integrable / dixonH2_tendsto_zero_of_integrable — the L¹ versions, via the shared estimate norm_integral_inv_sub_mul_le.

The decay of dixonH2 (hence of Dixon's glued function, which agrees with it far out) is the input to the Liouville step of Dixon's proof of the homology form of Cauchy's theorem (homologyCauchyTheorem, TauCetiRoadmap/ContourIntegration/Suggested.lean).

Provenance

Adapted from dixonH2_norm_le and dixonH2_tendsto_zero in DixonTheorem.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval (the |b - a| factor is the interval length, invisible in the [0, 1]-parametrised original). The L¹ variants additionally shed the boundedness hypothesis, bounding by ∫ ‖f (γ ·) * deriv γ‖ instead.

theorem TauCeti.Contour.dixonH2_norm_le {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b R M : ℝ} (hR : ∀ t ∈ Set.uIcc a b, ‖γ t‖ ≤ R) (hM : ∀ t ∈ Set.uIcc a b, ‖f (γ t) * deriv γ t‖ ≤ M) {w : ℂ} (hw : R < ‖w‖) : ‖dixonH2 f γ a b w‖ ≤ M / (‖w‖ - R) * |b - a|

Norm bound for dixonH2. When ‖w‖ > R, R bounds ‖γ‖, and M bounds the numerator product ‖f (γ ·) * deriv γ‖ on uIcc a b, the Cauchy-type integral is bounded by M / (‖w‖ - R) · |b - a|.

theorem TauCeti.Contour.dixonH2_tendsto_zero {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b R M : ℝ} (hR : ∀ t ∈ Set.uIcc a b, ‖γ t‖ ≤ R) (hM : ∀ t ∈ Set.uIcc a b, ‖f (γ t) * deriv γ t‖ ≤ M) : Filter.Tendsto (dixonH2 f γ a b) (Filter.cocompact ℂ) (nhds 0)

dixonH2 f γ a b tends to 0 along cocompact ℂ. The norm bound dixonH2_norm_le has the form C / (‖w‖ - R) with C = M * |b - a|, so tendsto_zero_cocompact_of_norm_le_div applies.

theorem TauCeti.Contour.dixonH2_norm_le_of_integrable {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b R : ℝ} (hR : ∀ t ∈ Set.uIoc a b, ‖γ t‖ ≤ R) (hg : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) {w : ℂ} (hw : R < ‖w‖) : ‖dixonH2 f γ a b w‖ ≤ (∫ (t : ℝ) in Set.uIoc a b, ‖f (γ t) * deriv γ t‖) / (‖w‖ - R)

L¹ norm bound for dixonH2. When ‖w‖ > R, R bounds ‖γ‖ on Ι a b, and the weight f (γ ·) * deriv γ is interval-integrable, dixonH2 is bounded by that weight's L¹ norm divided by ‖w‖ - R. Unlike dixonH2_norm_le this needs no uniform bound on the integrand, so it applies to raw curves whose derivative is only interval-integrable: rewrite the integrand as (γ t - w)⁻¹ * (f (γ t) * deriv γ t) and apply norm_integral_inv_sub_mul_le. Only the bound on the half-open interval Ι a b is needed.

theorem TauCeti.Contour.dixonH2_tendsto_zero_of_integrable {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b R : ℝ} (hR : ∀ t ∈ Set.uIoc a b, ‖γ t‖ ≤ R) (hg : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) : Filter.Tendsto (dixonH2 f γ a b) (Filter.cocompact ℂ) (nhds 0)

dixonH2 f γ a b tends to 0 along cocompact ℂ (L¹ form). The L¹ norm bound dixonH2_norm_le_of_integrable is already of the form C / (‖w‖ - R), so tendsto_zero_cocompact_of_norm_le_div applies; the interval-integrable weight replaces the uniform bound of dixonH2_tendsto_zero.