The local exponential series

Let K be a finite extension of ℚ_[p], with absolute ramification index e. At every integral depth i satisfying e < (p - 1) * i, the exponential series

∑ n, x ^ n / n !

converges for x ∈ 𝓂[K] ^ i, and this file proves that convergence. Its sum is Mathlib's NormedSpace.exp, so no new exponential is introduced here.

The threshold e < (p - 1) * i is exactly the range in which the term valuations tend to infinity throughout the ideal: there the normalized valuation of x ^ n / n ! grows linearly in n for every x ∈ 𝓂[K] ^ i, so the series converges on all of 𝓂[K] ^ i rather than on a smaller ball. The strictness matters: at e = (p - 1) * i an x of normalized valuation exactly i has x ^ n / n ! of valuation i * s with s the sum of the base p digits of n, so the term valuations stay bounded along n = p ^ k and the terms do not tend to zero. Convergence on the whole ideal is what makes the exponential a map from the deep additive group 𝓂[K] ^ i to the deep unit group 1 + 𝓂[K] ^ i, whose inverse is the logarithm; that identification of a deep additive group with a deep unit group is what computes the power classes, and hence the square classes, of K.

Main results

• TauCeti.tendsto_expSeries_term_zero_of_le_normalizedValuation: exponential terms tend to zero when the argument has sufficiently large normalized valuation.
• TauCeti.summable_expSeries_of_mem_maximalIdeal_pow: the exponential series is summable on 𝓂[K] ^ i in the convergence range.
• TauCeti.hasSum_exp_of_mem_maximalIdeal_pow: on 𝓂[K] ^ i in the convergence range the exponential series sums to NormedSpace.exp.
• TauCeti.exp_add_of_mem_maximalIdeal_pow: exp (x + y) = exp x * exp y on 𝓂[K] ^ i.

References

• J.-P. Serre, Local Fields, Chapter II, §5.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5.

theorem TauCeti.tendsto_expSeries_term_zero_of_le_normalizedValuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} {x : K} (hx : x ≠ 0) (hxi : ↑i ≤ Multiplicative.toAdd ((normalizedValuation K) (Units.mk0 x hx))) (hi : absoluteRamificationIndex K p < (p - 1) * i) : Filter.Tendsto (fun (n : ℕ) => x ^ n / ↑n.factorial) Filter.atTop (nhds 0)

At a depth in the exponential convergence range, the terms x ^ n / n ! tend to zero for every nonzero x whose normalized valuation is at least that depth.

theorem TauCeti.summable_expSeries_of_mem_maximalIdeal_pow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) (hi : absoluteRamificationIndex K p < (p - 1) * i) : Summable fun (n : ℕ) => ↑↑x ^ n / ↑n.factorial

The exponential series is summable for an element of 𝓂[K] ^ i whenever e(K/ℚ_p) < (p - 1) * i.

theorem TauCeti.hasSum_exp_of_mem_maximalIdeal_pow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) (hi : absoluteRamificationIndex K p < (p - 1) * i) : HasSum (fun (n : ℕ) => ↑↑x ^ n / ↑n.factorial) (NormedSpace.exp ↑↑x)

The exponential series of a deep element sums to Mathlib's exponential NormedSpace.exp.

theorem TauCeti.exp_add_of_mem_maximalIdeal_pow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) (x y : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) : NormedSpace.exp (↑↑x + ↑↑y) = NormedSpace.exp ↑↑x * NormedSpace.exp ↑↑y

The functional equation of the exponential on deep elements. On 𝓂[K] ^ i with (p - 1) * i > e, exp (x + y) = exp x * exp y.