Spectral cutoffs of a positive operator

For a positive operator A : E →L[ℂ] E and a level s : ℝ the spectral cutoff is the positive part of A - s, and the spectral cocutoff is the positive part of s - A, both formed with the continuous functional calculus:

A.spectralCutoff s = (A - s)₊,   A.spectralCocutoff s = (s - A)₊.

Their point is that the closed subspace ker (A.spectralCutoff s) splits E exactly the way the spectral projection of A for [0, s] would, without needing a projection-valued measure:

• on ker (A.spectralCutoff s), A is bounded above by s;
• on its orthogonal complement, A is bounded below by s.

That is all the spectral theorem is used for in the min--max theorem for approximation numbers, so with these two lemmas that theorem needs no measure theory — see ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxUpper.lean.

The two inequalities

Both come from a pointwise inequality of real functions fed to cfc_nonneg, so neither needs A to be compact, E to be separable, or any spectral decomposition to exist.

For the upper bound, t * t - s ^ 2 ≤ (t + s) * max (t - s) 0 holds for every t ≥ 0 — with equality when t ≥ s and with a negative left side otherwise. Reading it through the functional calculus gives A * A ≤ s ^ 2 + (A + s) * (A - s)₊, and the second summand annihilates the kernel of the cutoff, leaving ‖A y‖ ^ 2 ≤ s ^ 2 * ‖y‖ ^ 2 there.

For the lower bound, (s - t) ≤ max (s - t) 0 gives s - A ≤ (s - A)₊. The cocutoff kills the orthogonal complement of the kernel — its range lies in the kernel, because max (t - s) 0 * max (s - t) 0 = 0 identically, and it is self-adjoint, so it preserves the complement as well — leaving s * ‖y‖ ^ 2 ≤ re ⟪A y, y⟫, and Cauchy--Schwarz finishes.

The smooth cutoff, and why there are two of them

TauCeti.tailCutoff u is a continuous profile — 1 - u² / max x u² — vanishing below u² and tending to 1 above it, and norm_comp_cfc_one_sub_tailCutoff_le and mul_norm_cfc_tailCutoff_le_norm_apply are the same pair of inequalities for it, stated for the Gram operator S⋆S of an operator between two spaces rather than for a positive operator on one.

A kernel cutoff and a multiplier cutoff are not interchangeable, and the difference is what the real min--max theorem turns on. ker (A.spectralCutoff s) is a subspace; the orthogonal projection onto it need not be a continuous function of A. A multiplier cfc f A is one by construction, so it commutes with everything A commutes with — in particular with a conjugation, which is exactly what lets the cutoff descend from a complexification to a real operator. That is why ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxReal.lean cannot reuse the kernel pair and needs this one.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForTauCeti; it has had no prior home. The smooth cutoff section arrived later, from ForTauCeti/Analysis/OperatorIdeal/ApproximationNumber/MinMaxReal.lean, where it had been written private against one Hilbert space; it is stated here for any.
• Extraction class: authored in place for the Tau Ceti staging layer.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none. vendor/Spectra proves the corresponding facts through its projection-valued-measure and Borel functional calculus layer; the point of this module is that the continuous functional calculus already in Mathlib suffices.

The smooth cutoff profile

spectralCutoff below cuts by a kernel; this section builds the ingredients for cutting by a continuous multiplier instead. The two do the same job and are not interchangeable: a multiplier that is a continuous function of the operator commutes with everything the operator does, and in particular survives a conjugation, which a kernel projection need not.

noncomputable def TauCeti.tailCutoff (u x : ℝ) : ℝ

A continuous cutoff which vanishes at energies at most u², tends to one at high energy, and gives a tail operator bounded by u.

Named tailCutoff rather than spectralCutoff because ContinuousLinearMap.spectralCutoff in this same module is a different object — the positive part of A - s, an operator, where this is the scalar profile a smooth multiplier is built from.

Equations

• TauCeti.tailCutoff u x = 1 - u ^ 2 / max x (u ^ 2)

theorem TauCeti.continuous_tailCutoff (u : ℝ) (hu : 0 < u) : Continuous (tailCutoff u)

The profile is continuous, which is the whole reason for choosing it: only a continuous function of an operator is available to the continuous functional calculus. The denominator max x (u ^ 2) never vanishes for 0 < u, which is what makes the quotient continuous everywhere rather than only away from 0.

theorem TauCeti.tailCutoff_eq_zero_of_le {u x : ℝ} (hu : 0 < u) (hx : x ≤ u ^ 2) : tailCutoff u x = 0

Below the threshold the profile is identically zero, so the multiplier annihilates the low end of the spectrum exactly rather than merely damping it.

theorem TauCeti.tailCutoff_tail_bound {u x : ℝ} (hu : 0 < u) (_hx0 : 0 ≤ x) : x * (1 - tailCutoff u x) ^ 2 ≤ u ^ 2

The bound the cutoff was designed for. The complementary profile 1 - tailCutoff u is supported below u ^ 2 and decays like u ^ 2 / x above it, so x times its square never exceeds u ^ 2. Fed to the functional calculus this says the low-energy piece of an operator has norm at most u.

theorem TauCeti.tailCutoff_lower_bound {u x : ℝ} (hu : 0 < u) : u ^ 2 * tailCutoff u x ^ 2 ≤ x * tailCutoff u x ^ 2

On the support of the profile the argument is at least u ^ 2, so multiplying by the square of the profile only increases what u ^ 2 would give. This is the bound behind the lower modulus on the high end of the spectrum.

noncomputable def ContinuousLinearMap.spectralCutoff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (s : ℝ) : E →L[ℂ] E

The positive part (A - s)₊ of A - s, formed with the continuous functional calculus.

Equations

• A.spectralCutoff s = cfc (fun (t : ℝ) => max (t - s) 0) A

noncomputable def ContinuousLinearMap.spectralCocutoff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (s : ℝ) : E →L[ℂ] E

The positive part (s - A)₊ of s - A, formed with the continuous functional calculus.

Equations

• A.spectralCocutoff s = cfc (fun (t : ℝ) => max (s - t) 0) A

theorem ContinuousLinearMap.cutoff_split {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : 0 ≤ A) (s : ℝ) : s ^ 2 • 1 + (A + s • 1) * A.spectralCutoff s - A * A = cfc (fun (t : ℝ) => s ^ 2 + (t + s) * max (t - s) 0 - t * t) A

The operator identity behind the upper bound: s ^ 2 + (A + s) (A - s)₊ - A ^ 2 is the functional calculus of a single real function.

theorem ContinuousLinearMap.cocutoff_split {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : 0 ≤ A) (s : ℝ) : A.spectralCocutoff s - (s • 1 - A) = cfc (fun (t : ℝ) => max (s - t) 0 - (s - t)) A

The operator identity behind the lower bound.

theorem ContinuousLinearMap.spectralCutoff_mul_spectralCocutoff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : 0 ≤ A) (s : ℝ) : A.spectralCutoff s * A.spectralCocutoff s = 0

The cutoff and the cocutoff annihilate each other: the real functions defining them have disjoint supports.

theorem ContinuousLinearMap.isSelfAdjoint_spectralCocutoff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : 0 ≤ A) (s : ℝ) : IsSelfAdjoint (A.spectralCocutoff s)

The complementary spectral cut-off is self-adjoint, hence an orthogonal projection.

@[simp]

theorem ContinuousLinearMap.spectralCutoff_spectralCocutoff_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : 0 ≤ A) (s : ℝ) (x : E) : (A.spectralCutoff s) ((A.spectralCocutoff s) x) = 0

The range of the cocutoff lies in the kernel of the cutoff.

theorem ContinuousLinearMap.norm_apply_le_of_spectralCutoff_apply_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {A : E →L[ℂ] E} (hA : 0 ≤ A) {s : ℝ} (hs : 0 ≤ s) {y : E} (hy : (A.spectralCutoff s) y = 0) : ‖A y‖ ≤ s * ‖y‖

A is bounded above by s on the kernel of its s-cutoff.

theorem ContinuousLinearMap.le_norm_apply_of_mem_orthogonal_ker_spectralCutoff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {A : E →L[ℂ] E} (hA : 0 ≤ A) {s : ℝ} {y : E} (hy : y ∈ (↑(A.spectralCutoff s)).kerᗮ) : s * ‖y‖ ≤ ‖A y‖

A is bounded below by s on the orthogonal complement of the kernel of its s-cutoff.

theorem ContinuousLinearMap.cfc_mul_self_mul_eq_cfc_mul_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {C : E →L[ℂ] E} (hC : IsSelfAdjoint C) {p : ℝ → ℝ} (hpcont : Continuous p) : cfc p C * C * cfc p C = cfc (fun (x : ℝ) => x * p x ^ 2) C

Compressing C by cfc p C is the calculus applied to x * p x ^ 2.

Both cutoff bounds below need this, at p = tailCutoff u and at p = 1 - tailCutoff u, and each had written the same four-step calc out in full.

theorem ContinuousLinearMap.cfc_sub_sq_mul_eq_compression_sub_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {C : E →L[ℂ] E} (hC : IsSelfAdjoint C) {p : ℝ → ℝ} (hpcont : Continuous p) (u : ℝ) : cfc (fun (x : ℝ) => (x - u ^ 2) * p x ^ 2) C = cfc p C * C * cfc p C - u ^ 2 • (cfc p C * cfc p C)

A weighted spectral identity, read through the continuous functional calculus.

The pointwise identity (x - u ^ 2) * p x ^ 2 = x * p x ^ 2 - u ^ 2 * p x ^ 2 becomes an operator identity: the left side is cfc p C * C * cfc p C, the compression of C by cfc p C, and the right side is u ^ 2 times cfc p C ^ 2.

Nothing here is about cutoffs. p is any continuous real function and u any real number, which is why this is stated on its own rather than inline: the cutoff lemma below uses it at p = tailCutoff u, and the argument never looks at what p is.

theorem ContinuousLinearMap.norm_comp_cfc_one_sub_tailCutoff_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (S : E →L[ℂ] F) {u : ℝ} (hu : 0 < u) : ‖S ∘SL cfc (fun (x : ℝ) => 1 - TauCeti.tailCutoff u x) (adjoint S ∘SL S)‖ ≤ u

Cutting an operator to the low end of its spectrum leaves norm at most u.

cfc (1 - tailCutoff u) C, for the Gram operator C = S⋆S, is the multiplier that keeps the part of the spectrum at or below u ^ 2. Composing S with it gives an operator whose own Gram operator is x * (1 - tailCutoff u x) ^ 2, and the cutoff was chosen so that the functional calculus bounds that by u ^ 2.

This is the smooth counterpart of norm_apply_le_of_spectralCutoff_apply_eq_zero above, which splits by a kernel instead. A smooth multiplier is not a stylistic preference: the consumer is the real min--max theorem, which works on a complexification and needs its cutoff to descend to a real operator, and only a continuous function of C is conjugation-fixed.

theorem ContinuousLinearMap.mul_norm_cfc_tailCutoff_le_norm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (S : E →L[ℂ] F) {u : ℝ} (hu : 0 < u) (z : E) : u * ‖(cfc (TauCeti.tailCutoff u) (adjoint S ∘SL S)) z‖ ≤ ‖S ((cfc (TauCeti.tailCutoff u) (adjoint S ∘SL S)) z)‖

On the high end of the spectrum the modulus is bounded below by u.

The complement of the previous cutoff, cfc (tailCutoff u) C, lands where the Gram operator is at least u ^ 2. The quadratic form of cfc ((x - u ^ 2) * tailCutoff u x ^ 2) C is nonnegative there, and reading that form through S is the stated inequality.

This is the smooth counterpart of le_norm_apply_of_mem_orthogonal_ker_spectralCutoff above.