Crouzeix--Palencia assembly from auxiliary-operator bounds #
This file isolates two algebraic routes to the Crouzeix--Palencia constant.
The project-specific sharp-product route assumes that, for F = p(A), an
auxiliary operator G satisfies
‖F + G⋆‖ ≤ 2m, and‖F G‖ ≤ m²,
then the C⋆-identity gives the quadratic inequality
‖F‖² ≤ 2m‖F‖ + m², hence ‖F‖ ≤ (1 + √2)m.
This sharp product bound is not the invariant used in the published 2017
proof. The Crouzeix--Palencia argument, in the shorter
Ransford--Schwenninger formulation, instead combines a contractive scalar
Cauchy-transform companion with an a priori finite norm K for the whole
functional calculus. Its fourth-power bootstrap gives
K⁴ ≤ 2K³ + K², hence the same constant. Both algebraic endpoints are
formalized below; their distinct analytic hypotheses remain explicit.
Main declarations #
norm_le_one_add_sqrt_two_mul_of_auxiliary_bounds-- the C⋆-algebraic quadratic estimate.norm_fourth_power_le_of_companion_calculus_bounds-- the published Ransford--Schwenninger fourth-power bridge from a contractive companion and a global functional-calculus bound.norm_fourth_power_le_of_polynomial_companion_calculus_bounds-- the exact polynomial-companion specialization, including the multiplicative triple estimate from compact-set sup norms.norm_fourth_power_le_of_tendsto_polynomial_companions-- passage from uniformly contractive polynomial companions to their operator-norm limit.le_one_add_sqrt_two_of_fourth_le_two_mul_cube_add_sq-- the scalar fixed point which closes that bridge.crouzeix_palencia_of_global_polynomial_bound_of_fourth_power-- its exact polynomial spectral-set capstone.four_mul_re_inner_mul_eq_norm_adjoint_add_sq_sub-- the exact symmetric minus antisymmetric quadratic-form identity for the auxiliary product.two_smul_remainder_add_adjoint_eq_main_sub_symmetric_sq_add_skew_sq-- the corresponding exact Hermitian decomposition of a separated remainder.re_inner_mul_lower_iff_norm_adjoint_sub_sq_le-- its sharp lower-bound reformulation as a relative skew contraction.crouzeix_palencia_of_auxiliary_bounds-- packages the estimate and the landed spectrum inclusion as a polynomial spectral-set result.crouzeix_palencia_of_polynomial_auxiliary_bounds-- specializes that package to the contour operator constructed inAuxOperator.lean.crouzeix_palencia_of_isStarNormal-- the sharper normal-operator branch.
The algebraic core of the Crouzeix--Palencia estimate. The identity
F F⋆ = F (F + G⋆)⋆ - F G, the C⋆-identity, and the two assumed auxiliary
bounds give a quadratic inequality whose positive root is (1 + √2) m.
The exact C⋆-identity behind the short Ransford--Schwenninger version of
the Crouzeix--Palencia argument. In the intended application F = f(A) and
G = g(A), so multiplicativity identifies F * G * F with (f g f)(A).
The norm form of the Ransford--Schwenninger fourth-power identity. It
replaces a sharp standalone bound on F * G by control of the multiplicative
triple F * G * F, which is what a global functional-calculus norm supplies.
If a functional calculus has an a priori norm bound K, the companion is
symmetrically bounded by 2m, and multiplicativity plus companion contraction
bound F G F by K m³, then the published fourth-power estimate follows.
Taking K to be the best global calculus constant yields
K⁴ ≤ 2K³ + K², whose positive fixed point is 1 + √2.
Polynomial multiplicative triples #
Polynomial sup norms are submultiplicative on compact sets. Compactness
supplies the boundedness needed to compare each point evaluation with the
conditionally complete supremum used by polynomialSupNorm.
The compact-set sup norm of the multiplicative triple p*q*p is at
most ‖p‖²‖q‖.
A global polynomial-calculus bound controls the evaluated multiplicative triple by the product of the three compact-set polynomial sup norms. This is the algebraic approximation bridge needed when the scalar Cauchy companion has itself been represented by a polynomial.
The published fourth-power estimate specialized to a polynomial
companion q. A global calculus constant bounds both p(A) and the
multiplicative triple (p*q*p)(A); compact-set sup-norm
submultiplicativity and ‖p‖ₛ,‖q‖ₛ ≤ m give the required K m³ bound.
The analytic Crouzeix--Palencia companion need not be a polynomial, so using this theorem for that companion still requires a norm-preserving polynomial approximation argument.
Polynomial companion estimates pass to an operator-norm limit. If
q n (A) → G and every q n has sup norm at most m, then the global
polynomial-calculus bound controls p(A) G p(A) by K m³.
This statement isolates the exact approximation interface required for a holomorphic Cauchy companion: construction of the approximants and their uniform scalar bound are analytic inputs, while the limiting operator estimate is purely functional-analytic.
The published fourth-power estimate for an operator companion obtained as the operator-norm limit of uniformly sup-norm-bounded polynomial companions. This packages the limiting step needed after a norm-preserving polynomial approximation theorem for the scalar Cauchy companion.
A nonnegative global polynomial-calculus constant satisfying the
Ransford--Schwenninger fourth-power inequality is at most 1 + √2, and hence
gives the exact Crouzeix--Palencia polynomial spectral-set conclusion.
On any control set containing the spectrum, a finite polynomial-calculus bound together with a uniform fourth-power improvement closes the best-constant bootstrap. The proof takes the supremum of all normalized polynomial-calculus ratios, proves that this supremum is itself an admissible global constant, and applies the improvement at that exact constant.
A finite polynomial-calculus bound on the closed numerical range, together with a uniform fourth-power improvement, gives the exact Crouzeix--Palencia conclusion.
On a compact control set containing the spectrum, a finite global
polynomial-calculus bound and uniformly contractive polynomial approximants
to each auxiliary companion imply the (1 + √2) spectral-set bound.
A finite global polynomial-calculus bound and uniformly contractive polynomial approximants to each auxiliary companion imply the exact Crouzeix--Palencia conclusion. The operator-norm limit supplies the multiplicative triple estimate, while the preceding best-constant bootstrap globalizes its per-polynomial fourth-power improvement.
The Hermitian part of an auxiliary product is exactly the difference
between the squared symmetric and antisymmetric components. This is the
operator-vector form of the polarization identity
4 Re(FG) = (F† + G)†(F† + G) - (F† - G)†(F† - G); it requires no
commutation hypothesis.
If an auxiliary product is separated as F G = H - Q, then twice the
Hermitian remainder is exactly twice the Hermitian main term, minus the
symmetric square, plus the antisymmetric square. Thus positivity of the
double-layer/Kadison part and control of the skew part are distinct pieces;
no triangle inequality or commutation hypothesis enters this identity.
The one-sided product estimate used in the Palencia balance is exactly a relative bound on the antisymmetric auxiliary component.
The Crouzeix--Palencia balance only uses the lower real part of the
auxiliary product. In the identity
F F† = F (F + G†)† - F G, an upper bound for F F† requires only
-m² ≤ re ⟪x, F G x⟫ on unit vectors. No bound on the modulus, numerical
radius, or operator norm of F G is needed.
The Crouzeix--Palencia balance only needs the product estimate on
unit-vector quadratic forms. Evaluating
F F† = F (F + G†)† - F G at a unit vector bounds ‖F† x‖; normalization
then recovers the operator norm. Thus a numerical-radius bound on F G
is sufficient for the exact (1 + √2) constant.
A relative contraction of the antisymmetric auxiliary component is the
exact extra input needed beyond the symmetrized bound. By the polarization
identity above, bounding ‖(F† - G)x‖² by ‖(F† + G)x‖² + 4m² is equivalent
to the signed product estimate used by the sharp Palencia balance.
If every polynomial admits an auxiliary operator with the symmetrized
bound and the sharp product bound only on unit-vector quadratic forms, then
the closed numerical range is a (1 + √2)-polynomial spectral set.
If every polynomial admits an auxiliary operator with the symmetrized
bound and the sharp one-sided lower bound on the real part of its product,
then the closed numerical range is a (1 + √2)-polynomial spectral set.
If every polynomial admits an auxiliary operator satisfying the two
Crouzeix--Palencia bounds, then the closure of the numerical range is a
(1 + √2)-polynomial spectral set. This is the sorry-free assembly consumed
once L4.2c--e construct G and establish the bounds.
The L4.2d/e interface specialized to the contour operator from
AuxOperator.lean: once its symmetrized and product bounds hold for every
polynomial, the Crouzeix--Palencia spectral-set conclusion follows.
The Crouzeix--Palencia conclusion for a normal operator. In this branch
the sharper constant 1 follows from the continuous functional calculus and
the polynomial spectral mapping theorem; monotonicity then gives the stated
1 + √2 constant.