Supporting normals of smooth convex Jordan domains

At a regular point of a smooth convex boundary, the tangent line is a supporting line. Its two possible normal orientations are distinguished by the sign at any one point in the open carrier. This file formalizes that principle for the complex normal used by the Crouzeix--Palencia double-layer kernel.

The proof obtains an abstract supporting functional from Hahn--Banach. Its composition with the boundary trace has a maximum at the chosen parameter, so the functional annihilates the nonzero tangent. In the real plane, two linear functionals annihilating the same nonzero tangent are proportional. The sign at one carrier point makes the proportionality factor positive and therefore fixes the normal sign on the full frontier.

Main declarations

• SmoothJordanDomain.carrier_nonempty -- every represented domain has a nonempty carrier;
• SmoothJordanDomain.closure_support_and_carrier_strict_of_support_at_mem_carrier -- weak support on the closure and strict support in the open carrier;
• SmoothJordanDomain.canonicalNormal_support_all_of_support_at -- the canonical-normal sign at one carrier point and one parameter fixes the orientation globally;
• SmoothJordanDomain.frontier_support_of_support_at_mem_carrier -- the oriented normal sign at one carrier point propagates to the entire frontier;
• SmoothJordanDomain.reverseOrientation -- reversal of the boundary trace without changing the represented carrier;
• SmoothJordanDomain.canonicalOrientation -- a canonical choice between a trace and its reversal that has the supporting-normal sign.

theorem SmoothJordanDomain.carrier_nonempty (Omega : SmoothJordanDomain) : Omega.carrier.Nonempty

A smooth Jordan domain represented by a regular boundary trace has a nonempty open carrier. Otherwise its frontier would be empty, contradicting the nonempty range of the trace.

theorem SmoothJordanDomain.closure_support_and_carrier_strict_of_support_at_mem_carrier (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (t : ℝ) (hcside : ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) : (∀ z ∈ closure Omega.carrier, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (z - Omega.boundaryParam t)).re ≤ 0) ∧ ∀ z ∈ Omega.carrier, ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (z - Omega.boundaryParam t)).re < 0

At a regular trace point of a smooth convex Jordan domain, the canonical complex normal is nonpositive on the closed carrier and strictly negative on the open carrier as soon as its nonpositive sign is known at one carrier point.

theorem SmoothJordanDomain.canonicalNormal_support_all_of_support_at (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (t0 : ℝ) (hcside : ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t0) * (c - Omega.boundaryParam t0)).re ≤ 0) (t : ℝ) : ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0

For a smooth strictly convex Jordan trace, the canonical-normal sign at one point of the open carrier cannot change along the parameter line. It is strict at the carrier point, never vanishes at any parameter, and continuity then rules out a sign change by the intermediate value theorem.

theorem SmoothJordanDomain.frontier_support_of_support_at_mem_carrier (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (t : ℝ) (hcside : ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (xi : ℂ) : xi ∈ frontier Omega.carrier → ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (xi - Omega.boundaryParam t)).re ≤ 0

At a regular trace point of a smooth convex Jordan domain, the canonical complex normal has a constant oriented sign on the frontier as soon as that sign is known at one point of the open carrier.

noncomputable def SmoothJordanDomain.reverseOrientation (Omega : SmoothJordanDomain) : SmoothJordanDomain

Reverse the orientation of a smooth Jordan boundary by the affine reparametrization t ↦ 2π - t. The carrier and all of its geometric properties are unchanged.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SmoothJordanDomain.reverseOrientation_carrier (Omega : SmoothJordanDomain) : Omega.reverseOrientation.carrier = Omega.carrier

@[simp]

theorem SmoothJordanDomain.reverseOrientation_boundaryParam (Omega : SmoothJordanDomain) (t : ℝ) : Omega.reverseOrientation.boundaryParam t = Omega.boundaryParam (2 * Real.pi - t)

theorem SmoothJordanDomain.deriv_reverseOrientation_boundaryParam (Omega : SmoothJordanDomain) (t : ℝ) : deriv Omega.reverseOrientation.boundaryParam t = -deriv Omega.boundaryParam (2 * Real.pi - t)

noncomputable def SmoothJordanDomain.orientationPointSupport (Omega : SmoothJordanDomain) : ℂ

A chosen interior point used to distinguish the two boundary orientations.

Equations

• Omega.orientationPointSupport = Classical.choose ⋯

noncomputable def SmoothJordanDomain.canonicalOrientation (Omega : SmoothJordanDomain) : SmoothJordanDomain

Choose the original boundary orientation when its canonical normal points outward at a fixed carrier point, and choose the reversed orientation otherwise.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SmoothJordanDomain.canonicalOrientation_carrier (Omega : SmoothJordanDomain) : Omega.canonicalOrientation.carrier = Omega.carrier

theorem SmoothJordanDomain.exists_oriented_point_canonicalOrientation (Omega : SmoothJordanDomain) : ∃ c ∈ Omega.canonicalOrientation.carrier, ((starRingEnd ℂ) (-Complex.I * deriv Omega.canonicalOrientation.boundaryParam 0) * (c - Omega.canonicalOrientation.boundaryParam 0)).re ≤ 0

The canonical orientation has an interior point whose canonical normal has the supporting sign at parameter zero.