The dual stage norms and the disc norms of Amice transforms

A locally analytic distribution μ on ℤ_p is recorded by its moments bₙ = μ (x ↦ (x choose n)), the coefficients of its Amice transform F = ∑ bₙ Tⁿ. Restricted to the functions analytic on the discs of radius p⁻ʰ, μ has the dual stage norm

D_h(F) = supₙ ‖bₙ‖ ‖⌊n / pʰ⌋!‖,

computed in ℚ_p: Amice's basis of that stage consists of the polynomials ⌊n / pʰ⌋! (x choose n). On the analytic side, F has the Gauss norm S_h(F) = supₙ ‖bₙ‖ r_hⁿ at the radius

r_h = p ^ (-1 / ((p - 1) pʰ)),

which is the pʰ-th root of the radius p ^ (-1 / (p - 1)) of convergence of the p-adic exponential. Legendre's formula (p - 1) v_p(m!) = m - s_p(m) compares the two weights: r_hⁿ ≤ ‖⌊n / pʰ⌋!‖ ≤ p r_{h+1}ⁿ. Hence

S_h(F) ≤ D_h(F) ≤ p S_{h+1}(F),

each inequality holding as soon as its right-hand side is a supremum of a bounded family.

Since r_h increases to 1, every D_h(F) is finite exactly when every S_h(F) is finite, exactly when F converges on the open unit disc, that is, is restricted at every radius 0 < ρ < 1 (PowerSeries.OnOpenDisc). By Amice's theorem these are the coefficient conditions for F to be the Amice transform of a distribution. A bound at a single level does not suffice: the moments 1 / n! of the exponential series have finite level-zero norm but infinite level-one norm. The series log (1 + T), with coefficients (-1) ^ (n + 1) / n, lies on the open unit disc (PowerSeries.onOpenDisc_log), but its coefficients are unbounded, so it is not the Amice transform of a measure. Informally, it is the transform of the derivative at zero, a distribution that is not a measure.

The supremum amiceDualNorm is a real iSup, so its value is meaningful only for bounded families; every statement assumes the relevant boundedness. The disc norm S_h is Mathlib's PowerSeries.gaussNorm at the radius TauCeti.amiceRadius p h.

Main definitions

• TauCeti.amiceRadius p h: the radius p ^ (-1 / ((p - 1) pʰ)).
• TauCeti.amiceDualNorm p h F: the dual stage norm supₙ ‖coeff n F‖ ‖⌊n / pʰ⌋!‖, with the basic API TauCeti.le_amiceDualNorm and TauCeti.amiceDualNorm_le.

Main results

• TauCeti.amiceRadius_pow_le_norm_factorial, TauCeti.norm_factorial_le_mul_amiceRadius_succ_pow: r_hⁿ ≤ ‖⌊n / pʰ⌋!‖ ≤ p r_{h+1}ⁿ.
• TauCeti.norm_factorial_pow_eq_mul_amiceRadius_pow: along n = p^(h + k) the lower bound is sharp up to the factor p ^ (1 / (p - 1)).
• TauCeti.gaussNorm_amiceRadius_le_amiceDualNorm: S_h(F) ≤ D_h(F).
• TauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ: D_h(F) ≤ p S_{h+1}(F).
• TauCeti.onOpenDisc_iff_forall_hasGaussNorm_amiceRadius and TauCeti.onOpenDisc_iff_forall_bddAbove_norm_coeff_mul_norm_factorial: all disc norms, equivalently all dual stage norms, are finite exactly when the series lies on the open unit disc.
• TauCeti.memℓp_factorial_mul_coeff_of_onOpenDisc: on the open unit disc of a normed ℚ_p-algebra, the weighted coefficients ⌊n / pʰ⌋! coeff n F are bounded at every level.
• TauCeti.bddAbove_norm_coeff_mul_norm_factorial_zero_exp and TauCeti.not_bddAbove_norm_coeff_mul_norm_factorial_one_exp: the exponential series has finite dual stage norm at level zero but not at level one.
• TauCeti.not_bddAbove_norm_coeff_log and TauCeti.log_notMem_range_amiceTransform: the coefficients of log (1 + T) are unbounded in ℚ_p, so it is not the Amice transform of a measure.

References

• Y. Amice, Interpolation p-adique, Bull. Soc. Math. France 92 (1964), 117–180.
• P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), §I.4 and §II.2.
• J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, §3, Theorem 3.43.

The radii r_h

noncomputable def TauCeti.amiceRadius (p h : ℕ) : ℝ

The radius r_h = p ^ (-1 / ((p - 1) pʰ)) attached to the analytic level h: the pʰ-th root of the radius of convergence p ^ (-1 / (p - 1)) of the p-adic exponential. The Gauss norm of an Amice transform at this radius is comparable with its dual stage norm at level h.

theorem TauCeti.amiceRadius_def (p h : ℕ) : amiceRadius p h = ↑p ^ (-(1 / ((↑p - 1) * ↑p ^ h)))

The closed form of the radius r_h.

theorem TauCeti.amiceRadius_pos {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) : 0 < amiceRadius p h

The radii r_h are positive.

theorem TauCeti.amiceRadius_lt_one {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) : amiceRadius p h < 1

The radii r_h are smaller than 1.

theorem TauCeti.amiceRadius_pow {p : ℕ} (h n : ℕ) : amiceRadius p h ^ n = ↑p ^ (-(↑n / ((↑p - 1) * ↑p ^ h)))

The n-th power of r_h is p ^ (-n / ((p - 1) pʰ)).

theorem TauCeti.amiceRadius_zero_pow_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] : amiceRadius p 0 ^ (p - 1) = (↑p)⁻¹

r_0 ^ (p - 1) = p⁻¹: the radius r_0 = p ^ (-1 / (p - 1)) is the radius of convergence of the p-adic exponential.

theorem TauCeti.amiceRadius_succ_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) : amiceRadius p (h + 1) ^ p = amiceRadius p h

r_{h+1} ^ p = r_h: each radius is the p-th root of the previous one.

theorem TauCeti.strictMono_amiceRadius {p : ℕ} [hp : Fact (Nat.Prime p)] : StrictMono (amiceRadius p)

The radii r_h increase strictly with the level h.

theorem TauCeti.tendsto_amiceRadius {p : ℕ} [hp : Fact (Nat.Prime p)] : Filter.Tendsto (amiceRadius p) Filter.atTop (nhds 1)

The radii r_h tend to 1.

The weights ‖⌊n / pʰ⌋!‖

theorem TauCeti.amiceRadius_pow_le_norm_factorial {p : ℕ} [hp : Fact (Nat.Prime p)] (h n : ℕ) : amiceRadius p h ^ n ≤ ‖↑(n / p ^ h).factorial‖

Lower weight bound. r_hⁿ ≤ ‖⌊n / pʰ⌋!‖: the weight r_hⁿ of the Gauss norm at the radius r_h is at most the weight of the dual stage norm at level h.

theorem TauCeti.norm_factorial_le_mul_amiceRadius_succ_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (h n : ℕ) : ‖↑(n / p ^ h).factorial‖ ≤ ↑p * amiceRadius p (h + 1) ^ n

Upper weight bound. ‖⌊n / pʰ⌋!‖ ≤ p r_{h+1}ⁿ: the weight of the dual stage norm at level h is at most p times the weight r_{h+1}ⁿ of the Gauss norm at the radius r_{h+1}.

theorem TauCeti.norm_factorial_pow_eq_mul_amiceRadius_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (h k : ℕ) : ‖↑(p ^ k).factorial‖ = ↑p ^ (1 / (↑p - 1)) * amiceRadius p h ^ p ^ (h + k)

The lower weight bound is sharp up to a constant. Along n = p^(h + k), where ⌊n / pʰ⌋ = pᵏ, the weight ‖(pᵏ)!‖ is p ^ (1 / (p - 1)) r_hⁿ. So r_hⁿ / ‖⌊n / pʰ⌋!‖ does not tend to zero, and no bound ρⁿ ≤ ‖⌊n / pʰ⌋!‖ holds for all n with ρ > r_h.

The dual stage norm and its comparison with the disc norms

noncomputable def TauCeti.amiceDualNorm (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] (h : ℕ) (F : PowerSeries K) : ℝ

The dual stage norm D_h(F) = supₙ ‖coeff n F‖ ‖⌊n / pʰ⌋!‖ of a power series F, the factorials being taken in ℚ_p. When F is the Amice transform of a distribution, Amice's basis theorem identifies it with the norm of the distribution on the functions analytic on the discs of radius p⁻ʰ. As a real supremum it is meaningful only when the family is bounded above.

theorem TauCeti.amiceDualNorm_def {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] (h : ℕ) (F : PowerSeries K) : amiceDualNorm p h F = ⨆ (n : ℕ), ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖

The dual stage norm is the supremum of the terms ‖coeff n F‖ ‖⌊n / pʰ⌋!‖.

theorem TauCeti.norm_coeff_mul_amiceRadius_pow_le {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] (F : PowerSeries K) (h n : ℕ) : ‖(PowerSeries.coeff n) F‖ * amiceRadius p h ^ n ≤ ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖

The lower weight bound, multiplied by the norm of a coefficient: the term of the Gauss norm at the radius r_h is at most the term of the dual stage norm at level h.

theorem TauCeti.norm_coeff_mul_norm_factorial_le {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] (F : PowerSeries K) (h n : ℕ) : ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖ ≤ ↑p * (‖(PowerSeries.coeff n) F‖ * amiceRadius p (h + 1) ^ n)

The upper weight bound, multiplied by the norm of a coefficient: the term of the dual stage norm at level h is at most p times the term of the Gauss norm at the radius r_{h+1}.

theorem TauCeti.le_amiceDualNorm {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ} (hF : BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖)) (n : ℕ) : ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖ ≤ amiceDualNorm p h F

Each term of a bounded family is at most the dual stage norm.

theorem TauCeti.amiceDualNorm_le {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ} {C : ℝ} (hC : ∀ (n : ℕ), ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖ ≤ C) : amiceDualNorm p h F ≤ C

A common bound on the terms bounds the dual stage norm.

theorem TauCeti.amiceDualNorm_nonneg {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] (h : ℕ) (F : PowerSeries K) : 0 ≤ amiceDualNorm p h F

The dual stage norm is nonnegative.

theorem TauCeti.hasGaussNorm_amiceRadius_of_bddAbove {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ} (hF : BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖)) : PowerSeries.HasGaussNorm norm (amiceRadius p h) F

A bounded dual stage norm at level h bounds the Gauss norm at the radius r_h.

theorem TauCeti.bddAbove_norm_coeff_mul_norm_factorial_of_hasGaussNorm {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ} (hF : PowerSeries.HasGaussNorm norm (amiceRadius p (h + 1)) F) : BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖)

A bounded Gauss norm at the radius r_{h+1} bounds the dual stage norm at level h.

theorem TauCeti.gaussNorm_amiceRadius_le_amiceDualNorm {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ} (hF : BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖)) : PowerSeries.gaussNorm norm (amiceRadius p h) F ≤ amiceDualNorm p h F

S_h ≤ D_h. The Gauss norm at the radius r_h is at most the dual stage norm at level h, provided the latter is the supremum of a bounded family.

theorem TauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ} (hF : PowerSeries.HasGaussNorm norm (amiceRadius p (h + 1)) F) : amiceDualNorm p h F ≤ ↑p * PowerSeries.gaussNorm norm (amiceRadius p (h + 1)) F

D_h ≤ p S_{h+1}. The dual stage norm at level h is at most p times the Gauss norm at the radius r_{h+1}, provided the latter is the supremum of a bounded family.

Finiteness at every level

theorem TauCeti.onOpenDisc_iff_forall_isRestricted_amiceRadius {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} : PowerSeries.OnOpenDisc 1 F ↔ ∀ (h : ℕ), PowerSeries.IsRestricted (amiceRadius p h) F

A series lies on the open unit disc exactly when it is restricted at every radius r_h.

theorem TauCeti.onOpenDisc_iff_forall_hasGaussNorm_amiceRadius {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} : PowerSeries.OnOpenDisc 1 F ↔ ∀ (h : ℕ), PowerSeries.HasGaussNorm norm (amiceRadius p h) F

All disc norms are finite exactly on the open unit disc. A series has a finite Gauss norm at every radius r_h exactly when it is restricted at every radius 0 < ρ < 1.

theorem TauCeti.onOpenDisc_iff_forall_bddAbove_norm_coeff_mul_norm_factorial {p : ℕ} [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} : PowerSeries.OnOpenDisc 1 F ↔ ∀ (h : ℕ), BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖)

All dual stage norms are finite exactly on the open unit disc. The families ‖coeff n F‖ ‖⌊n / pʰ⌋!‖ are bounded for every level h exactly when F is restricted at every radius 0 < ρ < 1.

theorem TauCeti.memℓp_factorial_mul_coeff_of_onOpenDisc (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedRing K] {F : PowerSeries K} [NormedAlgebra ℚ_[p] K] [NormOneClass K] (hF : PowerSeries.OnOpenDisc 1 F) (h : ℕ) : Memℓp (fun (n : ℕ) => ↑(n / p ^ h).factorial * (PowerSeries.coeff n) F) ⊤

Weighted coefficients on the open unit disc are bounded. If F lies on the open unit disc of a normed ℚ_p-algebra K with ‖1‖ = 1, then at every level h the family ⌊n / pʰ⌋! coeff n F, the factorials being taken in K, is bounded.

Examples: the exponential and the logarithm

theorem TauCeti.bddAbove_norm_coeff_mul_norm_factorial_zero_exp {p : ℕ} [hp : Fact (Nat.Prime p)] : BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) (PowerSeries.exp ℚ_[p])‖ * ‖↑(n / p ^ 0).factorial‖)

The moments 1 / n! of the exponential series have a finite dual stage norm at level zero: every term ‖1 / n!‖ ‖n!‖ is 1.

theorem TauCeti.not_bddAbove_norm_coeff_mul_norm_factorial_one_exp {p : ℕ} [hp : Fact (Nat.Prime p)] : ¬BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) (PowerSeries.exp ℚ_[p])‖ * ‖↑(n / p ^ 1).factorial‖)

A bound at one level does not suffice. The moments 1 / n! of the exponential series have an infinite dual stage norm at level one: the term at n = p k is ‖k!‖ / ‖(p k)!‖ = pᵏ.

theorem TauCeti.not_onOpenDisc_exp {p : ℕ} [hp : Fact (Nat.Prime p)] : ¬PowerSeries.OnOpenDisc 1 (PowerSeries.exp ℚ_[p])

The exponential series does not lie on the open unit disc of ℚ_p: its dual stage norm at level one is infinite.

theorem TauCeti.not_bddAbove_norm_coeff_log {p : ℕ} [hp : Fact (Nat.Prime p)] : ¬BddAbove (Set.range fun (n : ℕ) => ‖(PowerSeries.coeff n) (PowerSeries.log ℚ_[p])‖)

The coefficients of log (1 + T) are unbounded in ℚ_p: the coefficient of T ^ (p ^ k) has norm pᵏ. By contrast, log (1 + T) lies on the open unit disc (PowerSeries.onOpenDisc_log).

theorem TauCeti.log_notMem_range_amiceTransform {p : ℕ} [hp : Fact (Nat.Prime p)] : PowerSeries.log ℚ_[p] ∉ AbstractMeasure.amiceTransform.range

log (1 + T) is not the Amice transform of a measure. The series log (1 + T) is not the Amice transform of a bounded measure on ℤ_p with values in ℚ_p, its coefficients being unbounded. Informally, it is the transform of the derivative at zero, which is therefore a distribution but not a measure.