Circle-model symmetrized Crouzeix–Palencia bound (L4.2d assembly)

Let A be an operator whose numerical range closure lies in the open disk ball c R, and let B t = (-i γ'(t)) • R_A(γ(t)), γ = circleMap c R, be the double-layer circle kernel. Given the double-layer representation p(A) + G† = (2π)⁻¹ ∫₀^{2π} p(γ(t)) • (B t + (B t)†) dt and the circle Cauchy identity ∫₀^{2π} γ'(t) • R_A(γ(t)) dt = 2πi • 1, the symmetrized bound ‖p(A) + G†‖ ≤ 2 * sup_{|z - c| ≤ R} ‖p(z)‖ follows from the positive-kernel contractivity (SymmetrizedBound.lean, PositiveKernelBound.lean): the kernel B + B† is positive (DoubleLayer.lean), has mass 4π (DoubleLayerIntegral.lean), and is integrable (CircleKernel.lean).

The two analytic inputs are taken as explicit hypotheses in the main theorem; the circle Cauchy identity is discharged (for C(0, R) with ‖A‖ < R) by CircleCauchy.lean in the final corollary, and the representation is the polynomial double-layer identity of SymmetrizedAuxiliary.lean.

Main declarations

• norm_eval_circleMap_le_polynomialSupNorm_closedBall — the scalar bound on the circle.
• intervalIntegrable_deriv_circleMap_smul_resolvent — integrability of the Cauchy integrand.
• norm_aeval_add_star_le_two_mul_polynomialSupNorm_of_representation — the bound.
• norm_aeval_add_star_le_two_mul_polynomialSupNorm_of_representation_of_norm_lt — the bound for the circle C(0, R) with ‖A‖ < R, where the Cauchy identity is discharged by CircleCauchy.lean and only the representation hypothesis remains.
• norm_aeval_add_star_crouzeixPolynomialAuxiliaryOperator_ball_le — the unconditional disk-model bound: for ‖A‖ < R and the auxiliary operator G of SmoothJordanDomain.ball 0 R, ‖p(A) + G†‖ ≤ 2 * sup_{|z| ≤ R} ‖p(z)‖ (representation from SymmetrizedAuxiliary.lean).
• norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_closedBall_of_aux_eq — the disk-model Crouzeix–Palencia inequality ‖p(A)‖ ≤ (1 + √2) * sup_{|z| ≤ R} ‖p(z)‖, given the value G = star (p.eval 0) • 1 of the disk auxiliary operator (the product bound of CircleProduct.lean and the balance identity of Palencia.lean).
• norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_closedBall_of_norm_lt — the unconditional disk-model Crouzeix–Palencia inequality: for ‖A‖ < R and every polynomial p, ‖p(A)‖ ≤ (1 + √2) * sup_{|z| ≤ R} ‖p(z)‖ (auxiliary-operator value from CircleAuxiliary.lean).

theorem norm_eval_circleMap_le_polynomialSupNorm_closedBall (p : Polynomial ℂ) (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (t : ℝ) : ‖Polynomial.eval (circleMap c R t) p‖ ≤ polynomialSupNorm p (Metric.closedBall c R)

On the circle |z - c| = R (with 0 ≤ R), a polynomial is bounded by its sup-norm over the closed disk closedBall c R.

theorem intervalIntegrable_deriv_circleMap_smul_resolvent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) : IntervalIntegrable (fun (t : ℝ) => deriv (circleMap c R) t • resolvent A (circleMap c R t)) MeasureTheory.volume 0 (2 * Real.pi)

The Cauchy integrand γ'(t) • R_A(γ(t)) along a circle in the resolvent set is interval integrable over [0, 2π].

theorem norm_aeval_add_star_le_two_mul_polynomialSupNorm_of_representation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hW : closure (numericalRange A) ⊆ Metric.ball c R) (p : Polynomial ℂ) (G : E →L[ℂ] E) (hrep : (Polynomial.aeval A) p + star G = (2 * Real.pi)⁻¹ • ∫ (t : ℝ) in 0..2 * Real.pi, Polynomial.eval (circleMap c R t) p • ((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t) + ContinuousLinearMap.adjoint ((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t)))) (hCauchy : ∫ (t : ℝ) in 0..2 * Real.pi, deriv (circleMap c R) t • resolvent A (circleMap c R t) = (2 * ↑Real.pi * Complex.I) • 1) : ‖(Polynomial.aeval A) p + star G‖ ≤ 2 * polynomialSupNorm p (Metric.closedBall c R)

Circle-model symmetrized Crouzeix–Palencia bound, given the double-layer representation of p(A) + G† and the circle Cauchy identity for the resolvent: if the closure of the numerical range of A lies in the open disk ball c R, then ‖p(A) + G†‖ ≤ 2 * sup_{|z - c| ≤ R} ‖p(z)‖.

Discharging the Cauchy identity on C(0, R) for ‖A‖ < R

theorem closure_numericalRange_subset_ball_of_norm_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) : closure (numericalRange A) ⊆ Metric.ball 0 R

If ‖A‖ < R, the closure of the numerical range lies in the open disk ball 0 R.

theorem intervalIntegral_deriv_circleMap_smul_resolvent_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) : ∫ (t : ℝ) in 0..2 * Real.pi, deriv (circleMap 0 R) t • resolvent A (circleMap 0 R t) = (2 * ↑Real.pi * Complex.I) • 1

The un-normalized circle Cauchy identity ∫₀^{2π} γ'(t) • R_A(γ(t)) dt = 2πi • 1 for γ = circleMap 0 R, ‖A‖ < R.

theorem norm_aeval_add_star_le_two_mul_polynomialSupNorm_of_representation_of_norm_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) (G : E →L[ℂ] E) (hrep : (Polynomial.aeval A) p + star G = (2 * Real.pi)⁻¹ • ∫ (t : ℝ) in 0..2 * Real.pi, Polynomial.eval (circleMap 0 R t) p • ((-Complex.I * deriv (circleMap 0 R) t) • resolvent A (circleMap 0 R t) + ContinuousLinearMap.adjoint ((-Complex.I * deriv (circleMap 0 R) t) • resolvent A (circleMap 0 R t)))) : ‖(Polynomial.aeval A) p + star G‖ ≤ 2 * polynomialSupNorm p (Metric.closedBall 0 R)

Circle-model symmetrized Crouzeix–Palencia bound for ‖A‖ < R, given the double-layer representation of p(A) + G†: ‖p(A) + G†‖ ≤ 2 * sup_{|z| ≤ R} ‖p(z)‖.

The unconditional disk-model bound

theorem norm_aeval_add_star_crouzeixPolynomialAuxiliaryOperator_ball_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball 0 R ⋯) p)‖ ≤ 2 * polynomialSupNorm p (Metric.closedBall 0 R)

Disk-model symmetrized Crouzeix–Palencia bound. For ‖A‖ < R and the auxiliary operator G of the disk ball 0 R, ‖p(A) + G†‖ ≤ 2 * sup_{|z| ≤ R} ‖p(z)‖.

The disk-model Crouzeix–Palencia inequality, given the auxiliary-operator value

theorem norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_closedBall_of_aux_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) (hG : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball 0 R ⋯) p = star (Polynomial.eval 0 p) • 1) : ‖(Polynomial.aeval A) p‖ ≤ (1 + √2) * polynomialSupNorm p (Metric.closedBall 0 R)

Disk-model Crouzeix–Palencia inequality, given the value of the disk auxiliary operator: if ‖A‖ < R and the conjugate-polynomial auxiliary operator of ball 0 R equals star (p.eval 0) • 1, then ‖p(A)‖ ≤ (1 + √2) * sup_{|z| ≤ R} ‖p(z)‖.

The unconditional disk-model Crouzeix–Palencia inequality

theorem norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_closedBall_of_norm_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ (1 + √2) * polynomialSupNorm p (Metric.closedBall 0 R)

Disk-model Crouzeix–Palencia inequality. If ‖A‖ < R, then for every polynomial p, ‖p(A)‖ ≤ (1 + √2) * sup_{|z| ≤ R} ‖p(z)‖.