Complex-affine invariance of the boundary double-layer density

A nonconstant complex-affine map z ↦ a * z + b carries a smooth strictly convex Jordan domain to another such domain while preserving its boundary parameter. The logarithmic-derivative factors contributed by a cancel, so the scalar boundary double-layer density is pointwise invariant when its base point is transported by the same map.

Consequently, integrability, total mass, and nonnegativity of the density all transport exactly. In particular, an oriented double-layer probability density on the original frontier gives sharp boundary-phase contractivity for every polynomial on any translate, rotation, or nonzero scaling of the domain.

Main declarations

• SmoothJordanDomain.complexAffine -- the transported smooth Jordan domain;
• SmoothJordanDomain.frontier_complexAffine -- its frontier is the image of the original frontier;
• crouzeixBoundaryDoubleLayerDensity_complexAffine -- pointwise density invariance;
• integral_crouzeixBoundaryDoubleLayerDensity_complexAffine -- exact mass transport;
• crouzeixBoundaryPhaseContractive_complexAffine_of_boundaryDoubleLayerProbability -- sharp phase contractivity on the image from the original probability density.

noncomputable def SmoothJordanDomain.complexAffine (Omega : SmoothJordanDomain) (a b : ℂ) (ha : a ≠ 0) : SmoothJordanDomain

The image of a smooth Jordan domain under the nonconstant complex-affine map z ↦ a * z + b, with its boundary parametrization transported by the same map.

Equations

• Omega.complexAffine a b ha = (Omega.linearImage (ContinuousLinearEquiv.smulLeft (Units.mk0 a ha))).translate b

@[simp]

theorem SmoothJordanDomain.complexAffine_carrier (Omega : SmoothJordanDomain) (a b : ℂ) (ha : a ≠ 0) : (Omega.complexAffine a b ha).carrier = (fun (z : ℂ) => a * z + b) '' Omega.carrier

@[simp]

theorem SmoothJordanDomain.complexAffine_boundaryParam (Omega : SmoothJordanDomain) (a b : ℂ) (ha : a ≠ 0) : (Omega.complexAffine a b ha).boundaryParam = fun (t : ℝ) => a * Omega.boundaryParam t + b

theorem SmoothJordanDomain.frontier_complexAffine (Omega : SmoothJordanDomain) (a b : ℂ) (ha : a ≠ 0) : frontier (Omega.complexAffine a b ha).carrier = (fun (z : ℂ) => a * z + b) '' frontier Omega.carrier

The frontier of a complex-affine image is exactly the image of the original frontier.

theorem crouzeixBoundaryDoubleLayerDensity_complexAffine (Omega : SmoothJordanDomain) (a b xi : ℂ) (ha : a ≠ 0) (t : ℝ) : crouzeixBoundaryDoubleLayerDensity (Omega.complexAffine a b ha) (a * xi + b) t = crouzeixBoundaryDoubleLayerDensity Omega xi t

Simultaneously transporting the domain and base point by a nonconstant complex-affine map leaves the scalar double-layer density unchanged.

theorem intervalIntegrable_crouzeixBoundaryDoubleLayerDensity_complexAffine_iff (Omega : SmoothJordanDomain) (a b xi : ℂ) (ha : a ≠ 0) : IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity (Omega.complexAffine a b ha) (a * xi + b)) MeasureTheory.volume 0 (2 * Real.pi) ↔ IntervalIntegrable (crouzeixBoundaryDoubleLayerDensity Omega xi) MeasureTheory.volume 0 (2 * Real.pi)

Interval integrability of the transported density is equivalent to that of the original density.

theorem integral_crouzeixBoundaryDoubleLayerDensity_complexAffine (Omega : SmoothJordanDomain) (a b xi : ℂ) (ha : a ≠ 0) : ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity (Omega.complexAffine a b ha) (a * xi + b) t = ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t

The total interval-integral mass of the double-layer density is invariant under nonconstant complex-affine transport.

theorem crouzeixBoundaryPhaseContractive_complexAffine_of_boundaryDoubleLayerProbability (Omega : SmoothJordanDomain) (a b : ℂ) (ha : a ≠ 0) (p : Polynomial ℂ) (hmass : ∀ xi ∈ frontier Omega.carrier, ∫ (t : ℝ) in 0..2 * Real.pi, crouzeixBoundaryDoubleLayerDensity Omega xi t = 1) (hpos : ∀ xi ∈ frontier Omega.carrier, ∀ t ∈ Set.Ioc 0 (2 * Real.pi), 0 ≤ crouzeixBoundaryDoubleLayerDensity Omega xi t) : CrouzeixBoundaryPhaseContractive (Omega.complexAffine a b ha) p

If the original frontier carries a pointwise nonnegative unit-mass double-layer density, then every polynomial satisfies the sharp boundary phase estimate on every nonconstant complex-affine image of the domain.