Negative powers of the distance to a point, integrated along a segment

A function with an algebraic singularity at a point p is still integrable along a segment passing arbitrarily close to p, provided the exponent is larger than -1. This file proves the quantitative form of that statement in ℂ, for use in the Schwarz--Christoffel boundary theory.

The geometric input is that on the segment from w to z, parametrized by [0, 1], the distance to p is at least the length of the segment times the distance of the parameter to a fixed parameter c, namely the foot of the perpendicular from p clamped to [0, 1]; the Cauchy--Schwarz inequality is what makes the comparison work. Both pieces of the parameter interval then compare with a power of the distance to c, whose integral Mathlib computes, and the singularity contributes only the finite constant 2 / (u + 1).

Main results

• Complex.exists_mem_Icc_mul_abs_sub_le_dist -- the lower bound for the distance to p along a segment.
• Complex.integral_dist_rpow_segment_le -- the arclength integral of dist ⬝ p ^ u along a segment of length L is at most 2 / (u + 1) * L ^ (u + 1) when -1 < u ≤ 0.

theorem Complex.exists_mem_Icc_mul_abs_sub_le_dist (p z w : ℂ) : ∃ c ∈ Set.Icc 0 1, ∀ s ∈ Set.Icc 0 1, ‖z - w‖ * |s - c| ≤ dist (w + s • (z - w)) p

On the segment from w to z, the distance to a point p is bounded below by the length of the segment times the distance of the parameter to a fixed parameter c ∈ [0, 1]. Geometrically c is the foot of the perpendicular from p, clamped to the parameter interval.

theorem Complex.integral_dist_rpow_segment_le {p : ℂ} {u : ℝ} (hu : -1 < u) (hu0 : u ≤ 0) {z w : ℂ} : (∫ (s : ℝ) in 0..1, dist (w + s • (z - w)) p ^ u) * ‖z - w‖ ≤ 2 / (u + 1) * ‖z - w‖ ^ (u + 1)

The arclength integral of a nonpositive power of the distance to p along the segment from w to z: the parameter integral over [0, 1] is multiplied by the length ‖z - w‖ of the segment. For -1 < u ≤ 0, the bound 2 / (u + 1) * ‖z - w‖ ^ (u + 1) is uniform in the position of p; in particular p is allowed to lie on the segment.