Continuity of Fredholm series in operator norm

A norm-convergent family of operators on C₀(I, R) whose entries share a null row majorant has determinants converging in every positive-radius Gauss norm; in particular so does a norm-convergent sequence of row-compact operators. This continuity permits finite determinant identities to pass to limits of row-compact operators. The finite identities apply to output truncations π_S ∘ u to a finite set S of coordinates, whose determinant is the polynomial determinant of the finite block of u on S (ContinuousLinearMap.charPowerSeries_matrixCoeff_indicatorCLM_comp). For a polynomial B with B(0) = 0, the determinant of B(π_S ∘ u) is likewise the polynomial det (1 - X B(A)) (ContinuousLinearMap.charPowerSeries_matrixCoeff_aeval_indicatorCLM_comp).

The determinant is u.matrixCoeff.charPowerSeries. Scalars may be complete ultrametric norm-one Tate rings, not just fields.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§4–5.

theorem ContinuousLinearMap.charPowerSeries_matrixCoeff_indicatorCLM_comp {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] (S : Finset I) (u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R) : (ZeroAtInftyContinuousMap.indicatorCLM R ↑S ∘SL u).matrixCoeff.charPowerSeries = ↑(u.matrixCoeff.submatrix Subtype.val Subtype.val).charpolyRev

The determinant of the output truncation π_S ∘ u to a finite set S is the polynomial det (1 - X A) for the finite block A of the matrix of u on S, since the rows of π_S ∘ u outside S vanish.

theorem ContinuousLinearMap.charPowerSeries_matrixCoeff_aeval_indicatorCLM_comp {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] (S : Finset I) (u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R) {B : Polynomial R} (hB0 : B.coeff 0 = 0) : ((Polynomial.aeval (ZeroAtInftyContinuousMap.indicatorCLM R ↑S ∘SL u)) B).matrixCoeff.charPowerSeries = ↑((Polynomial.aeval (u.matrixCoeff.submatrix Subtype.val Subtype.val)) B).charpolyRev

Spectral mapping for an output truncation. If B(0) = 0, the Fredholm determinant of B(π_S ∘ u) is the polynomial det (1 - T B(A)) for the block A of u on S, since the rows of B(π_S ∘ u) outside S vanish.

theorem TauCeti.tendsto_gaussNorm_charPowerSeries_sub_charPowerSeries_of_tendsto_ringOpNorm_of_le {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [IsUltrametricDist R] [NormedRing.IsTate R] [CompleteSpace R] {α : Type u_3} {l : Filter α} {w : α → ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} {w₀ : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} {r : I → ℝ} (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) (hw : ∀ (a : α) (i j : I), ‖(w a).matrixCoeff i j‖ ≤ r i) (hw₀ : ∀ (i j : I), ‖w₀.matrixCoeff i j‖ ≤ r i) (h : Filter.Tendsto (fun (a : α) => ‖w a - w₀‖) l (nhds 0)) {ρ : ℝ} (hρ : 0 < ρ) : Filter.Tendsto (fun (a : α) => PowerSeries.gaussNorm norm ρ ((w a).matrixCoeff.charPowerSeries - w₀.matrixCoeff.charPowerSeries)) l (nhds 0)

If operators w a on C₀(I, R) converge in operator norm to w₀, and all their entries are bounded by a common null row majorant r, then their Fredholm series converge in Gauss norm at every positive radius.

theorem TauCeti.tendsto_gaussNorm_charPowerSeries_sub_charPowerSeries_of_tendsto_ringOpNorm {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [IsUltrametricDist R] [NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} {v : ℕ → ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} [CompleteSpace R] (h : Filter.Tendsto (fun (n : ℕ) => ‖u - v n‖) Filter.atTop (nhds 0)) (hv : ∀ (n : ℕ), (v n).IsRowCompact) {ρ : ℝ} (hρ : 0 < ρ) : Filter.Tendsto (fun (n : ℕ) => PowerSeries.gaussNorm norm ρ ((v n).matrixCoeff.charPowerSeries - u.matrixCoeff.charPowerSeries)) Filter.atTop (nhds 0)

The Fredholm series of a norm-convergent sequence of row-compact operators converge in Gauss norm at every positive radius. Unlike coefficientwise convergence of arbitrary entire series, operator-norm convergence supplies uniform control of the determinant tails.