Induction through boundary-phase divided differences

At a frontier point xi, the sharp scalar-companion boundary estimate for a polynomial p contains the phase transform of p /ₘ (X - C xi). This quotient has strictly smaller degree whenever p has positive degree, but it depends on xi. Consequently the appropriate recursive invariant branches over every frontier point rather than following one fixed remainder polynomial.

This file packages that branching strong induction. The degree-zero base is already sharp because the divided difference vanishes. The resulting L4.2 connector leaves only a cancellation-preserving divided-difference-to-parent phase step as its phase hypothesis.

Main declarations

• CrouzeixBoundaryPhaseContractive -- the exact sharp frontier invariant;
• polynomial_induction_on_boundaryPhaseDividedDifferences -- branching strong induction through all frontier-dependent quotients;
• crouzeixBoundaryPhaseContractive_of_dividedDifference_induction -- the invariant with its degree-zero base discharged;
• crouzeixBoundaryPhaseContractive_of_normalized -- reduction to positive-degree polynomials of unit frontier sup norm;
• crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_induction -- the L4.2 assembly from the remaining positive-degree phase step.

def CrouzeixBoundaryPhaseContractive (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : Prop

The sharp boundary invariant for the scalar Crouzeix companion: at every frontier point, the conjugate point value plus the lower-degree phase contour is bounded by the polynomial frontier sup norm.

Equations

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

theorem SmoothJordanDomain.frontier_infinite (Omega : SmoothJordanDomain) : (frontier Omega.carrier).Infinite

Every smooth Jordan frontier is infinite. The boundary parametrization is injective on the infinite half-open fundamental interval, whose image lies in its full range.

theorem crouzeixBoundaryPhaseContractive_smul (Omega : SmoothJordanDomain) (a : ℂ) (p : Polynomial ℂ) (hp : CrouzeixBoundaryPhaseContractive Omega p) : CrouzeixBoundaryPhaseContractive Omega (a • p)

Phase contractivity is preserved by polynomial scaling. Both the boundary value and the frontier sup norm scale by the norm of the scalar.

theorem crouzeixBoundaryPhaseContractive_smul_iff (Omega : SmoothJordanDomain) {a : ℂ} (ha : a ≠ 0) (p : Polynomial ℂ) : CrouzeixBoundaryPhaseContractive Omega (a • p) ↔ CrouzeixBoundaryPhaseContractive Omega p

Scaling by a nonzero scalar preserves and reflects phase contractivity.

theorem polynomial_induction_on_boundaryPhaseDividedDifferences (Omega : SmoothJordanDomain) (P : Polynomial ℂ → Prop) (hzero : ∀ (p : Polynomial ℂ), p.natDegree = 0 → P p) (hstep : ∀ (p : Polynomial ℂ), 0 < p.natDegree → (∀ xi ∈ frontier Omega.carrier, P (p /ₘ (Polynomial.X - Polynomial.C xi))) → P p) (p : Polynomial ℂ) : P p

A branching strong-induction principle for the family of divided differences indexed by the frontier. Every quotient used in the positive degree step is strictly lower-degree.

theorem crouzeixBoundaryPhaseContractive_of_natDegree_eq_zero (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hp : p.natDegree = 0) : CrouzeixBoundaryPhaseContractive Omega p

Constant polynomials satisfy the sharp boundary-phase invariant.

theorem crouzeixBoundaryPhaseContractive_of_dividedDifference_induction (Omega : SmoothJordanDomain) (hstep : ∀ (p : Polynomial ℂ), 0 < p.natDegree → (∀ xi ∈ frontier Omega.carrier, CrouzeixBoundaryPhaseContractive Omega (p /ₘ (Polynomial.X - Polynomial.C xi))) → CrouzeixBoundaryPhaseContractive Omega p) (p : Polynomial ℂ) : CrouzeixBoundaryPhaseContractive Omega p

To establish sharp boundary-phase contractivity for every polynomial, it suffices to propagate it from all frontier-indexed divided differences to a positive-degree parent polynomial. The degree-zero base is automatic.

theorem crouzeixBoundaryPhaseContractive_of_normalized (Omega : SmoothJordanDomain) (hnormalized : ∀ (p : Polynomial ℂ), 0 < p.natDegree → polynomialSupNorm p (frontier Omega.carrier) = 1 → CrouzeixBoundaryPhaseContractive Omega p) (p : Polynomial ℂ) : CrouzeixBoundaryPhaseContractive Omega p

On the infinite compact frontier of a smooth Jordan domain, it suffices to prove phase contractivity for positive-degree polynomials normalized to frontier sup norm one. Exact conjugate homogeneity restores every nonzero scale, while the degree-zero case is automatic.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_boundaryPhase_induction {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hreg : ∀ (p : Polynomial ℂ) (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized (Omega n) p xi) (nhdsWithin xi (Omega n).carrier) (nhds (crouzeixPolynomialScalarCompanionRegularized (Omega n) p xi xi))) (hphaseStep : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → (∀ xi ∈ frontier (Omega n).carrier, CrouzeixBoundaryPhaseContractive (Omega n) (p /ₘ (Polynomial.X - Polynomial.C xi))) → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

The smooth-thickening scalar-companion route needs only a cancellation-preserving positive-degree induction step for the sharp phase invariant. Branching divided-difference induction supplies all-polynomial phase contractivity, after which the Plemelj assembly and fourth-power bootstrap give the exact Crouzeix--Palencia conclusion.

theorem crouzeix_palencia_of_convexThickening_cauchy_support_normalized_boundaryPhase {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : ℕ → SmoothJordanDomain) (hcarrier : ∀ (n : ℕ), (Omega n).carrier = convexThickeningApprox (closure (numericalRange A)) n) (hCauchyP : ∀ (p : Polynomial ℂ) (n : ℕ), (Polynomial.aeval A) p = (2 * ↑Real.pi * Complex.I)⁻¹ • contourIntegral (fun (z : ℂ) => Polynomial.eval z p • resolvent A z) (Omega n).boundaryParam) (hsupport : ∀ (n : ℕ), ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ∀ w ∈ numericalRange A, ((starRingEnd ℂ) (-Complex.I * deriv (Omega n).boundaryParam t) * (w - (Omega n).boundaryParam t)).re ≤ 0) (hkernel : ∀ (n : ℕ), ∀ z ∈ (Omega n).carrier, crouzeixScalarCauchyKernel (Omega n) z = 1) (hreg : ∀ (p : Polynomial ℂ) (n : ℕ), ∀ xi ∈ frontier (Omega n).carrier, Filter.Tendsto (crouzeixPolynomialScalarCompanionRegularized (Omega n) p xi) (nhdsWithin xi (Omega n).carrier) (nhds (crouzeixPolynomialScalarCompanionRegularized (Omega n) p xi xi))) (hphaseNormalized : ∀ (n : ℕ) (p : Polynomial ℂ), 0 < p.natDegree → polynomialSupNorm p (frontier (Omega n).carrier) = 1 → CrouzeixBoundaryPhaseContractive (Omega n) p) (happrox : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (r : ℕ → Polynomial ℂ), ∀ (j : ℕ), ∀ z ∈ compactThickeningApprox (closure (numericalRange A)) n, ‖Polynomial.eval z (r j) - crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p z‖ ≤ 1 / (↑j + 1)) (hPlemelj : ∀ (p : Polynomial ℂ) (n : ℕ), crouzeixAuxiliaryOperator A (Omega n) (crouzeixPolynomialScalarCompanionClosedExtension (Omega n) p) = crouzeixPolynomialAuxiliaryOperator A (Omega n) p) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Equivalently, the smooth-thickening scalar-companion route only needs the sharp phase theorem for positive-degree polynomials normalized to frontier sup norm one at each stage. Infinite-frontier normalization supplies all other scales and the constant case.