The boundary double-layer probability measure on a circle

For a positively oriented circle and a base point xi on that circle, the scalar boundary double-layer density is 1 / (2 pi) away from the unique parameter value representing xi and is zero at that parameter by the inverse-at-zero convention. The exceptional singleton has measure zero, so the density is nonnegative and has total mass one.

This completely discharges the geometric probability-measure interface in the disk model and recovers the sharp boundary-phase invariant for every polynomial through the general boundary-measure theorem.

Main declarations

• crouzeixBoundaryDoubleLayerDensity_ball_eq_inv_two_pi_of_ne -- the pointwise density away from the base point;
• integral_crouzeixBoundaryDoubleLayerDensity_ball -- its total mass is one;
• crouzeixBoundaryDoubleLayerDensity_ball_nonneg -- its pointwise sign;
• crouzeixBoundaryPhaseContractive_ball_of_boundaryDoubleLayerDensity -- sharp phase contractivity on every positive-radius disk.

theorem crouzeixBoundaryDoubleLayerDensity_ball_eq_inv_two_pi_of_ne {c xi : ℂ} {R : ℝ} (hR : 0 < R) (hxi : xi ∈ Metric.sphere c R) (t : ℝ) (hne : circleMap c R t ≠ xi) : crouzeixBoundaryDoubleLayerDensity (SmoothJordanDomain.ball c R hR) xi t = (2 * Real.pi)⁻¹

Away from its boundary base point, the double-layer density of a positive circle is the constant 1 / (2 pi).

theorem integral_crouzeixBoundaryDoubleLayerDensity_ball {c xi : ℂ} {R : ℝ} (hR : 0 < R) (hxi : xi ∈ Metric.sphere c R) : ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity (SmoothJordanDomain.ball c R hR) xi t = 1

The boundary double-layer density of a positive circle has total mass one at every boundary base point.

theorem crouzeixBoundaryDoubleLayerDensity_ball_nonneg {c xi : ℂ} {R : ℝ} (hR : 0 < R) (hxi : xi ∈ Metric.sphere c R) (t : ℝ) : 0 ≤ crouzeixBoundaryDoubleLayerDensity (SmoothJordanDomain.ball c R hR) xi t

The boundary double-layer density of a positive circle is everywhere nonnegative, including its inverse-at-zero value at the base point.

theorem crouzeixBoundaryPhaseContractive_ball_of_boundaryDoubleLayerDensity {c : ℂ} {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) : CrouzeixBoundaryPhaseContractive (SmoothJordanDomain.ball c R hR) p

Every polynomial satisfies the sharp boundary-phase invariant on a positive-radius disk, obtained from the explicit circle probability density.