Row Hodge lower polygons of principal-minor series

Let r : ι → ℝ be a bounded row majorant of a square matrix A, with ‖A i j‖ ≤ r i, and let r* be its decreasing rearrangement (TauCeti.decreasingRearrangement). For a base b > 1, the row Hodge polygon TauCeti.rowHodgePolygon b r is the height sequence

H n = ∑ k < n, -logb b (r* k)

on the integers n for which r* 0, …, r* (n - 1) are positive, and ⊤ elsewhere. Its finite domain is [0, m], where m is the number of positive entries of r, possibly infinite (TauCeti.rowHodgePolygon_ne_top_iff), and its slopes -logb b (r* k) are nondecreasing, so it is convex (TauCeti.isConvexSeq_rowHodgePolygon).

Fix a real additive valuation v on a normed field with ‖x‖ = b ^ (-v x) for x ≠ 0; a normalisation ‖x‖ = b ^ (-e w x) with e > 0 is the case v = e w. The coefficient estimate ‖cₙ‖ ≤ ∏ k < n, r* k of Matrix.norm_charCoeff_le_prod_decreasingRearrangement then says that the row Hodge polygon lies below every coefficient height of the principal-minor series A.charPowerSeries = ∑ cₙ Tⁿ, and hence below its Newton polygon (Matrix.rowHodgePolygon_le_newtonPolygon_charPowerSeries). Here cₙ is (-1) ^ n times the unconditional sum of the size-n principal minors (Matrix.charCoeff), and the estimates need no summability. When these families are summable, for instance when r tends to zero and the field is complete (Matrix.summable_principalMinor), the series is the Fredholm determinant det (1 - T A). Beyond m the coefficients vanish: for finite m the principal-minor series is a polynomial of degree at most m, possibly less. The row Hodge polygon depends on the chosen coordinates and majorant: it need not have the same right endpoint as the Newton polygon, and it is not the intrinsic Hodge polygon of a lattice.

A uniform bound ‖A i j‖ ≤ C gives the line of slope -logb b C through the origin below the Newton polygon (Matrix.isSupportingLine_newtonPolygon_charPowerSeries): every finite slope of the principal-minor series is at least -logb b C.

Main definitions

• TauCeti.rowHodgePolygon b r: the row Hodge polygon of the majorant r in base b.

Main results

• TauCeti.isConvexSeq_rowHodgePolygon, TauCeti.unitSlope_rowHodgePolygon: the polygon is convex with unit slopes -logb b (r* k).
• TauCeti.rowHodgePolygon_ne_top_iff: its finite domain is bounded by the number of positive entries of r.
• Matrix.rowHodgePolygon_le_addValuation_charCoeff, Matrix.rowHodgePolygon_le_newtonPolygon_charPowerSeries: it lies below the coefficient heights and the Newton polygon of the principal-minor series.
• Matrix.isSupportingLine_newtonPolygon_charPowerSeries: the slope bound from a uniform bound on the entries.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §5.
• K. S. Kedlaya, A little p-adic numerical analysis, MIT 18.787 notes (2007), §3.

noncomputable def TauCeti.rowHodgePolygon {ι : Type u_1} (b : ℝ) (r : ι → ℝ) (n : ℕ) : WithTop ℝ

The row Hodge polygon of a row majorant r in base b: the height ∑ k < n, -logb b (r* k) at n when the first n terms of the decreasing rearrangement r* of r are positive, and ⊤ otherwise.

theorem TauCeti.rowHodgePolygon_of_forall_lt {ι : Type u_1} {b : ℝ} {r : ι → ℝ} {n : ℕ} (h : ∀ k < n, 0 < decreasingRearrangement r k) : rowHodgePolygon b r n = ↑(∑ k ∈ Finset.range n, -Real.logb b (decreasingRearrangement r k))

Where the first n rearranged terms are positive, the row Hodge polygon is the sum of the first n slopes -logb b (r* k).

theorem TauCeti.rowHodgePolygon_eq_top_iff {ι : Type u_1} {b : ℝ} {r : ι → ℝ} {n : ℕ} : rowHodgePolygon b r n = ⊤ ↔ ∃ k < n, decreasingRearrangement r k ≤ 0

The row Hodge polygon is infinite at n exactly when one of the first n rearranged terms is not positive.

@[simp]

theorem TauCeti.rowHodgePolygon_apply_zero {ι : Type u_1} {b : ℝ} {r : ι → ℝ} : rowHodgePolygon b r 0 = 0

theorem TauCeti.rowHodgePolygon_ne_top_iff {ι : Type u_1} {b : ℝ} {r : ι → ℝ} {n : ℕ} (hr : BddAbove (Set.range r)) : rowHodgePolygon b r n ≠ ⊤ ↔ ∃ (s : Finset ι), s.card = n ∧ ∀ i ∈ s, 0 < r i

The row Hodge polygon is finite at n exactly when r has n positive entries. Its finite domain is therefore [0, m], where m is the number of positive entries, or all of ℕ when there are infinitely many.

theorem TauCeti.isConvexSeq_rowHodgePolygon {ι : Type u_1} {b : ℝ} {r : ι → ℝ} (hb : 1 < b) (hr : BddAbove (Set.range r)) : IsConvexSeq (rowHodgePolygon b r)

The row Hodge polygon is convex: its slopes -logb b (r* k) are nondecreasing because the rearrangement r* is antitone.

theorem TauCeti.unitSlope_rowHodgePolygon {ι : Type u_1} {b : ℝ} {r : ι → ℝ} {n : ℕ} (hr : BddAbove (Set.range r)) (hn : 0 < decreasingRearrangement r n) : unitSlope (rowHodgePolygon b r) n = -Real.logb b (decreasingRearrangement r n)

The unit slope of the row Hodge polygon at a positive rearranged term r* n is -logb b (r* n).

theorem TauCeti.isSupportingLine_rowHodgePolygon {ι : Type u_1} {b : ℝ} {r : ι → ℝ} (hb : 1 < b) {C : ℝ} (hC : ∀ (i : ι), r i ≤ C) : IsSupportingLine (rowHodgePolygon b r) (-Real.logb b C) 0

If every entry of r is at most C, the line of slope -logb b C through the origin lies below the row Hodge polygon.

theorem Matrix.rowHodgePolygon_le_addValuation_charCoeff {ι : Type u_1} {K : Type u_2} [DecidableEq ι] [NormedField K] [IsUltrametricDist K] {v : AddValuation K (WithTop ℝ)} {b : ℝ} {A : Matrix ι ι K} {r : ι → ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (hr : BddAbove (Set.range r)) (hA : ∀ (i j : ι), ‖A i j‖ ≤ r i) (n : ℕ) : TauCeti.rowHodgePolygon b r n ≤ v (A.charCoeff n)

The row Hodge polygon lies below the principal-minor coefficients. Let v be a real additive valuation with ‖x‖ = b ^ (-v x) for x ≠ 0, where b > 1. For a bounded row majorant ‖A i j‖ ≤ r i, the height of the n-th coefficient A.charCoeff n of the principal-minor series, no summability assumed, is at least the row Hodge polygon at n. In particular the coefficient vanishes when r has fewer than n positive entries.

theorem Matrix.rowHodgePolygon_le_newtonPolygon_charPowerSeries {ι : Type u_1} {K : Type u_2} [DecidableEq ι] [NormedField K] [IsUltrametricDist K] {v : AddValuation K (WithTop ℝ)} {b : ℝ} {A : Matrix ι ι K} {r : ι → ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) (hr : BddAbove (Set.range r)) (hA : ∀ (i j : ι), ‖A i j‖ ≤ r i) : TauCeti.rowHodgePolygon b r ≤ A.charPowerSeries.newtonPolygon v

Row Hodge lower bound for the principal-minor series. Let v be a real additive valuation with ‖x‖ = b ^ (-v x) for x ≠ 0, where b > 1. For a bounded row majorant ‖A i j‖ ≤ r i, the row Hodge polygon of r lies below the Newton polygon of the principal-minor series A.charPowerSeries, which is the Fredholm determinant det (1 - T A) when its principal-minor families are summable.

theorem Matrix.isSupportingLine_newtonPolygon_charPowerSeries {ι : Type u_1} {K : Type u_2} [DecidableEq ι] [NormedField K] [IsUltrametricDist K] {v : AddValuation K (WithTop ℝ)} {b : ℝ} {A : Matrix ι ι K} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {C : ℝ} (hA : ∀ (i j : ι), ‖A i j‖ ≤ C) : TauCeti.IsSupportingLine (A.charPowerSeries.newtonPolygon v) (-Real.logb b C) 0

Slope bound for the principal-minor series. Let v be a real additive valuation with ‖x‖ = b ^ (-v x) for x ≠ 0, where b > 1. If every entry of A has norm at most C, the line of slope -logb b C through the origin lies below the Newton polygon of the principal-minor series A.charPowerSeries, which is the Fredholm determinant det (1 - T A) when its principal-minor families are summable. Since that polygon starts at the origin, every finite slope is at least -logb b C.