Manifest-driven boundary for the landed operator-theory surface.

Every declaration below has an explicit type and delegates to the production declaration. A changed source signature therefore breaks elaboration, while the manifest separately audits the production declaration's axioms.

noncomputable def CrouzeixPalenciaBoundary.numericalRangeBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : Set ℂ

Numerical range exposed at the public boundary of the development.

Equations

• CrouzeixPalenciaBoundary.numericalRangeBoundary A = numericalRange A

theorem CrouzeixPalenciaBoundary.mem_numericalRange_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (z : ℂ) : z ∈ numericalRange A ↔ ∃ (x : E), ‖x‖ = 1 ∧ inner ℂ x (A x) = z

theorem CrouzeixPalenciaBoundary.norm_le_of_mem_numericalRange_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {z : ℂ} (hz : z ∈ numericalRange A) : ‖z‖ ≤ ‖A‖

theorem CrouzeixPalenciaBoundary.convex_numericalRange_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : Convex ℝ (numericalRange A)

noncomputable def CrouzeixPalenciaBoundary.polynomialSupNormBoundary (p : Polynomial ℂ) (X : Set ℂ) : ℝ

Polynomial supremum norm exposed at the public boundary.

Equations

• CrouzeixPalenciaBoundary.polynomialSupNormBoundary p X = polynomialSupNorm p X

def CrouzeixPalenciaBoundary.IsKPolynomialSpectralSetBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (K : ℝ) (X : Set ℂ) : Prop

Polynomial spectral-set estimate with a specified multiplicative constant.

Equations

• CrouzeixPalenciaBoundary.IsKPolynomialSpectralSetBoundary A K X = IsKPolynomialSpectralSet A K X

def CrouzeixPalenciaBoundary.IsPolynomialSpectralSetBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (X : Set ℂ) : Prop

Polynomial spectral-set estimate with constant one.

Equations

• CrouzeixPalenciaBoundary.IsPolynomialSpectralSetBoundary A X = IsPolynomialSpectralSet A X

theorem CrouzeixPalenciaBoundary.spectrum_subset_closure_numericalRange_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : spectrum ℂ A ⊆ closure (numericalRange A)

theorem CrouzeixPalenciaBoundary.numericalRange_adjoint_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : numericalRange (ContinuousLinearMap.adjoint A) = ⇑(starRingEnd ℂ) '' numericalRange A

theorem CrouzeixPalenciaBoundary.crouzeix_palencia_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Exact unconditional project capstone. This declaration is deliberately part of the manifest boundary so supporting lemmas cannot produce a vacuous green board while the final theorem is absent.

theorem CrouzeixPalenciaBoundary.exists_halmos_unitary_dilation_boundary {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) : ∃ U ∈ unitary (WithLp 2 (E × E) →L[ℂ] WithLp 2 (E × E)), ∀ (x : E), (U (WithLp.toLp 2 (x, 0))).fst = T x

theorem CrouzeixPalenciaBoundary.exists_unitary_power_dilation_boundary {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (V : E →L[ℂ] H) (U : H →L[ℂ] H), (∀ (x_3 y : E), inner ℂ (V x_3) (V y) = inner ℂ x_3 y) ∧ U ∈ unitary (H →L[ℂ] H) ∧ ∀ (n : ℕ) (x_3 : E), (ContinuousLinearMap.adjoint V) ((U ^ n) (V x_3)) = (T ^ n) x_3

theorem CrouzeixPalenciaBoundary.vonNeumann_inequality_boundary {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) (p : Polynomial ℂ) : ‖(Polynomial.aeval T) p‖ ≤ polynomialSupNorm p (Metric.closedBall 0 1)

def CrouzeixPalenciaBoundary.ContourIntegrableBoundary {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (γ : ℝ → ℂ) : Prop

Integrability along a parametrized complex contour.

Equations

• CrouzeixPalenciaBoundary.ContourIntegrableBoundary f γ = ContourIntegrable f γ

noncomputable def CrouzeixPalenciaBoundary.contourIntegralBoundary {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : ℂ → F) (γ : ℝ → ℂ) : F

The contour integral exposed at the public boundary.

Equations

• CrouzeixPalenciaBoundary.contourIntegralBoundary f γ = contourIntegral f γ

theorem CrouzeixPalenciaBoundary.contourIntegral_eq_zero_of_hasDerivAt_of_closed_boundary {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f Fp : ℂ → F} {γ : ℝ → ℂ} (hγ : ∀ t ∈ Set.Icc 0 (2 * Real.pi), DifferentiableAt ℝ γ t) (hF : ∀ t ∈ Set.Icc 0 (2 * Real.pi), HasDerivAt Fp (f (γ t)) (γ t)) (hint : ContourIntegrable f γ) (hclosed : γ (2 * Real.pi) = γ 0) : contourIntegral f γ = 0

theorem CrouzeixPalenciaBoundary.convexThickeningApprox_spec_boundary (K : Set ℂ) (hcompact : IsCompact K) (hconvex : Convex ℝ K) : (∀ (n : ℕ), K ⊆ convexThickeningApprox K n ∧ IsOpen (convexThickeningApprox K n) ∧ StrictConvex ℝ (convexThickeningApprox K n)) ∧ ⋂ (n : ℕ), convexThickeningApprox K n = K

noncomputable def CrouzeixPalenciaBoundary.smoothClosedBallApproximationBoundary (c : ℂ) (R : ℝ) (hR : 0 ≤ R) : SmoothConvexApproximation (Metric.closedBall c R)

Smooth convex approximations of a closed complex disk.

Equations

• CrouzeixPalenciaBoundary.smoothClosedBallApproximationBoundary c R hR = smoothClosedBallApproximation c R hR

noncomputable def CrouzeixPalenciaBoundary.crouzeixAuxiliaryOperatorBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (h : ℂ → ℂ) : E →L[ℂ] E

The contour auxiliary operator exposed at the public boundary.

Equations

• CrouzeixPalenciaBoundary.crouzeixAuxiliaryOperatorBoundary A Omega h = crouzeixAuxiliaryOperator A Omega h

noncomputable def CrouzeixPalenciaBoundary.crouzeixPolynomialAuxiliaryOperatorBoundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (p : Polynomial ℂ) : E →L[ℂ] E

The polynomial contour auxiliary operator exposed at the public boundary.

Equations

• CrouzeixPalenciaBoundary.crouzeixPolynomialAuxiliaryOperatorBoundary A Omega p = crouzeixPolynomialAuxiliaryOperator A Omega p

theorem CrouzeixPalenciaBoundary.exists_smoothJordanDomain_norm_bound_crouzeixPolynomialAuxiliaryOperator_boundary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (p : Polynomial ℂ) : ∃ (Omega : SmoothJordanDomain) (C : ℝ), closure (numericalRange A) ⊆ Omega.carrier ∧ ‖crouzeixPolynomialAuxiliaryOperator A Omega p‖ ≤ ‖(2 * ↑Real.pi * Complex.I)⁻¹‖ * (2 * Real.pi * C)