Similarity transport and normalization of the planar geometry problem

Smooth Jordan outer approximation is invariant under translations and nonzero complex similarities. The metric approximation scale changes by the similarity ratio, while the smooth Jordan structure itself is transported by the real-linear and translation constructors.

As a consequence, the remaining full-dimensional polytope problem can be normalized: it is enough to treat finite convex hulls containing a closed unit disk. An interior point supplies a small disk, and a homothety expands it to unit radius.

noncomputable def complexMulRealEquiv (a : ℂ) (ha : a ≠ 0) : ℂ ≃L[ℝ] ℂ

Multiplication by a nonzero complex number, regarded as an invertible real-linear map of the complex plane.

Equations

• complexMulRealEquiv a ha = ContinuousLinearEquiv.smulLeft (Units.mk0 a ha)

@[simp]

theorem complexMulRealEquiv_apply (a : ℂ) (ha : a ≠ 0) (z : ℂ) : (complexMulRealEquiv a ha) z = a * z

theorem closure_translate_linearImage_complexMulRealEquiv (Omega : SmoothJordanDomain) (c a : ℂ) (ha : a ≠ 0) : closure ((Omega.linearImage (complexMulRealEquiv a ha)).translate c).carrier = (fun (z : ℂ) => c + a * z) '' closure Omega.carrier

The closure of a smooth Jordan carrier transported by a complex similarity is the similarity image of the original closure.

theorem HasSmoothJordanOuterApproximation.similarity {K : Set ℂ} (hK : HasSmoothJordanOuterApproximation K) (c a : ℂ) (ha : a ≠ 0) : HasSmoothJordanOuterApproximation ((fun (z : ℂ) => c + a * z) '' K)

Smooth Jordan outer approximation is preserved by every nonzero complex similarity z ↦ c + a * z.

theorem homothety_apply_eq_const_add_mul (c z : ℂ) (r : ℝ) : (AffineMap.homothety c r) z = (1 - r) • c + ↑r * z

A real homothety written as a translation followed by scalar multiplication.

theorem HasSmoothJordanOuterApproximation.homothety {K : Set ℂ} (hK : HasSmoothJordanOuterApproximation K) (c : ℂ) (r : ℝ) (hr : r ≠ 0) : HasSmoothJordanOuterApproximation (⇑(AffineMap.homothety c r) '' K)

Smooth Jordan outer approximation is preserved by a nontrivial real homothety about any center.

def HasSmoothJordanOuterApproximationForUnitBallPolytopes : Prop

The normalized residual geometry problem: smooth outer approximation for every finite convex hull that contains a closed unit disk.

Equations

• HasSmoothJordanOuterApproximationForUnitBallPolytopes = ∀ (u : Finset ℂ) (c : ℂ), Metric.closedBall c 1 ⊆ (convexHull ℝ) ↑u → HasSmoothJordanOuterApproximation ((convexHull ℝ) ↑u)

theorem hasSmoothJordanOuterApproximationForPolytopes_of_unitBall_case (hunit : HasSmoothJordanOuterApproximationForUnitBallPolytopes) : HasSmoothJordanOuterApproximationForPolytopes

The unit-disk-normalized polytope case implies the unrestricted full-dimensional polytope case.

theorem crouzeix_palencia_of_smoothJordanOuterApproximation_unitBallPolytope_case {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (hunit : HasSmoothJordanOuterApproximationForUnitBallPolytopes) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The exact Crouzeix--Palencia bound follows once smooth outer approximation is proved for finite convex hulls containing a unit disk.