Ordered row bounds for Fredholm coefficients #
For a bounded row majorant r satisfying ‖A i j‖ ≤ r i on an arbitrary index type,
the norm of the n-th principal-minor coefficient is at most the product of the first n
terms of the decreasing rearrangement of r. For a null majorant, positive rearranged
terms are attained entries, with multiplicities retained and zeros padding finite support.
This is the coefficient estimate used to compare Fredholm Newton polygons with ordered
row bounds.
References #
- J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §5.
theorem
Matrix.norm_charCoeff_le_prod_decreasingRearrangement
{ι : Type u_1}
{R : Type u_2}
[DecidableEq ι]
[SeminormedCommRing R]
[NormOneClass R]
[IsUltrametricDist R]
{A : Matrix ι ι R}
{r : ι → ℝ}
(hr : BddAbove (Set.range r))
(hA : ∀ (i j : ι), ‖A i j‖ ≤ r i)
(n : ℕ)
:
The product of the first n terms of the decreasing rearrangement of a bounded row
majorant bounds the n-th Fredholm coefficient.
No enumeration of the row indices or infinitude of the positive row bounds is assumed.