feat(NumberTheory/Padics): Mahler coeffs tend to 0 (#19340)

This adds the key technical lemma in the proof of Mahler's theorem characterising continuous functions on Zp: for any continuous function, the iterated forward differences at 0 tend to zero.

Co-authored-by: Giulio Caflisch <[email protected]>

Mathlib/NumberTheory/Padics/MahlerBasis.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Giulio Caflisch, David Loeffler
 -/
+import Mathlib.Algebra.Group.ForwardDiff
 import Mathlib.Analysis.Normed.Group.Ultra
 import Mathlib.NumberTheory.Padics.ProperSpace
 import Mathlib.RingTheory.Binomial
@@ -15,15 +16,26 @@ import Mathlib.Topology.ContinuousMap.Compact
 In this file we introduce the Mahler basis function `mahler k`, for `k : ℕ`, which is the unique
 continuous map `ℤ_[p] → ℚ_[p]` agreeing with `n ↦ n.choose k` for `n ∈ ℕ`.
 
-In future PR's, we will show that these functions give a Banach basis for the space of continuous
-maps `ℤ_[p] → ℚ_[p]`.
+We also show that for any continuous function `f` on `ℤ_[p]` (valued in a `p`-adic normed space),
+the iterated forward differences `Δ^[n] f 0` tend to 0. For this, we follow the argument of
+Bojanić [bojanic74].
+
+In future PR's, we will show that the Mahler functions give a Banach basis for the space of
+continuous maps `ℤ_[p] → ℚ_[p]`, with the basis coefficients of `f` given by the forward differences
+`Δ^[n] f 0`.
 
 ## References
 
+* [R. Bojanić, *A simple proof of Mahler's theorem on approximation of continuous functions of a
+  p-adic variable by polynomials*][bojanic74]
 * [P. Colmez, *Fonctions d'une variable p-adique*][colmez2010]
+
+## Tags
+
+Bojanic
 -/
 
-open Finset
+open Finset fwdDiff IsUltrametricDist NNReal Filter Topology
 
 variable {p : ℕ} [hp : Fact p.Prime]
 
@@ -95,3 +107,134 @@ The uniform norm of the `k`-th Mahler basis function is 1, for every `k`.
   · -- Show norm 1 is attained at `x = k`
     refine (le_of_eq ?_).trans ((mahler k).norm_coe_le_norm k)
     rw [mahler_natCast_eq, Nat.choose_self, Nat.cast_one, norm_one]
+
+section fwdDiff
+
+variable {M G : Type*}
+
+/-- Bound for iterated forward differences of a continuous function from a compact space to a
+nonarchimedean seminormed group. -/
+lemma IsUltrametricDist.norm_fwdDiff_iter_apply_le [TopologicalSpace M] [CompactSpace M]
+    [AddCommMonoid M] [SeminormedAddCommGroup G] [IsUltrametricDist G]
+    (h : M) (f : C(M, G)) (m : M) (n : ℕ) : ‖Δ_[h]^[n] f m‖ ≤ ‖f‖ := by
+  -- A proof by induction on `n` would be possible but would involve some messing around to
+  -- define `Δ_[h]` as an operator on continuous maps (not just on bare functions). So instead we
+  -- use the formula for `Δ_[h]^[n] f` as a sum.
+  rw [fwdDiff_iter_eq_sum_shift]
+  refine norm_sum_le_of_forall_le_of_nonneg (norm_nonneg f) fun i _ ↦ ?_
+  exact (norm_zsmul_le _ _).trans (f.norm_coe_le_norm _)
+
+/-- First step in Bojanić's proof of Mahler's theorem (equation (10) of [bojanic74]): rewrite
+`Δ^[n + R] f 0` in a shape that makes it easy to bound `p`-adically. -/
+private lemma bojanic_mahler_step1 [AddCommMonoidWithOne M] [AddCommGroup G] (f : M → G)
+    (n : ℕ) {R : ℕ} (hR : 1 ≤ R) :
+    Δ_[1]^[n + R] f 0 = -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
+      ∑ k ∈ range (n + 1), ((-1 : ℤ) ^ (n - k) * n.choose k) • (f (k + R) - f k) := by
+  have aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0 := by
+    rw [Nat.sub_add_cancel hR, Nat.choose_self, one_smul]
+  rw [neg_add_eq_sub, eq_sub_iff_add_eq, add_comm, aux, (by omega : n + R = (n + ((R - 1) + 1))),
+    ← sum_range_succ, Nat.sub_add_cancel hR,
+    ← sub_eq_iff_eq_add.mpr (sum_range_succ' (fun x ↦ R.choose x • Δ_[1]^[n + x] f 0) R), add_zero,
+    Nat.choose_zero_right, one_smul]
+  have : ∑ k ∈ Finset.range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 = Δ_[1]^[n] f R := by
+    simpa only [← Function.iterate_add_apply, add_comm, nsmul_one, add_zero] using
+      (shift_eq_sum_fwdDiff_iter 1 (Δ_[1]^[n] f) R 0).symm
+  simp only [this, fwdDiff_iter_eq_sum_shift (1 : M) f n, mul_comm, nsmul_one, mul_smul, add_comm,
+    add_zero, smul_sub, sum_sub_distrib]
+
+end fwdDiff
+
+namespace PadicInt
+
+section norm_fwdDiff
+
+variable {p : ℕ} [hp : Fact p.Prime] {E : Type*}
+  [NormedAddCommGroup E] [NormedSpace ℚ_[p] E] [IsUltrametricDist E]
+
+/--
+Second step in Bojanić's proof of Mahler's theorem (equation (11) of [bojanic74]): show that values
+`Δ_[1]^[n + p ^ t] f 0` for large enough `n` are bounded by the max of `(‖f‖ / p ^ s)` and `1 / p`
+times a sup over values for smaller `n`.
+
+We use `nnnorm`s on the RHS since `Finset.sup` requires an order with a bottom element.
+-/
+private lemma bojanic_mahler_step2 {f : C(ℤ_[p], E)} {s t : ℕ}
+    (hst : ∀ x y : ℤ_[p], ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s) (n : ℕ) :
+    ‖Δ_[1]^[n + p ^ t] f 0‖ ≤ max ↑((Finset.range (p ^ t - 1)).sup
+      fun j ↦ ‖Δ_[1]^[n + (j + 1)] f 0‖₊ / p) (‖f‖ / p ^ s) := by
+  -- Use previous lemma to rewrite in a convenient form.
+  rw [bojanic_mahler_step1 _ _ (one_le_pow₀ hp.out.one_le)]
+  -- Now use ultrametric property and bound each term separately.
+  refine (norm_add_le_max _ _).trans (max_le_max ?_ ?_)
+  · -- Bounding the sum over `range (p ^ t - 1)`: every term involves a value `Δ_[1]^[·] f 0` and
+    -- a binomial coefficient which is divisible by `p`
+    rw [norm_neg, ← coe_nnnorm, coe_le_coe]
+    refine nnnorm_sum_le_of_forall_le (fun i hi ↦ Finset.le_sup_of_le hi ?_)
+    rw [mem_range] at hi
+    rw [← Nat.cast_smul_eq_nsmul ℚ_[p], nnnorm_smul, div_eq_inv_mul]
+    refine mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le])
+    -- remains to show norm of binomial coeff is `≤ p⁻¹`
+    have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by omega)
+    rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, Padic.norm_eq_pow_val (mod_cast this.ne'),
+      coe_zpow, NNReal.coe_natCast, (zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).le_iff_le,
+      neg_le_neg_iff, Padic.valuation_natCast, Nat.one_le_cast]
+    exact one_le_padicValNat_of_dvd this <| hp.out.dvd_choose_pow (by omega) (by omega)
+  · -- Bounding the sum over `range (n + 1)`: every term is small by the choice of `t`
+    refine norm_sum_le_of_forall_le_of_nonempty nonempty_range_succ (fun i _ ↦ ?_)
+    calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖
+    _ ≤ ‖f (i + ↑(p ^ t)) - f i‖ := by
+      rw [← Int.cast_smul_eq_zsmul ℚ_[p], norm_smul]
+      apply mul_le_of_le_one_left (norm_nonneg _)
+      simpa only [← coe_intCast] using norm_le_one _
+    _ ≤ ‖f‖ / p ^ s := by
+      apply hst
+      rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]
+
+/--
+Explicit bound for the decay rate of the Mahler coefficients of a continuous function on `ℤ_[p]`.
+This will be used to prove Mahler's theorem.
+ -/
+lemma fwdDiff_iter_le_of_forall_le {f : C(ℤ_[p], E)} {s t : ℕ}
+    (hst : ∀ x y : ℤ_[p], ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s) (n : ℕ) :
+    ‖Δ_[1]^[n + s * p ^ t] f 0‖ ≤ ‖f‖ / p ^ s := by
+  -- We show the following more general statement by induction on `k`:
+  suffices ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] f 0‖ ≤ ‖f‖ / p ^ k from this le_rfl
+  intro k hk
+  induction' k with k IH generalizing n
+  · -- base case just says that `‖Δ^[·] (⇑f) 0‖` is bounded by `‖f‖`
+    simpa only [zero_mul, pow_zero, add_zero, div_one] using norm_fwdDiff_iter_apply_le 1 f 0 n
+  · -- induction is the "step 2" lemma above
+    rw [add_mul, one_mul, ← add_assoc]
+    refine (bojanic_mahler_step2 hst (n + k * p ^ t)).trans (max_le ?_ ?_)
+    · rw [← coe_nnnorm, ← NNReal.coe_natCast, ← NNReal.coe_pow, ← NNReal.coe_div, NNReal.coe_le_coe]
+      refine Finset.sup_le fun j _ ↦ ?_
+      rw [pow_succ, ← div_div, div_le_div_iff_of_pos_right (mod_cast hp.out.pos), add_right_comm]
+      exact_mod_cast IH (n + (j + 1)) (by omega)
+    · exact div_le_div_of_nonneg_left (norm_nonneg _)
+        (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk)
+
+/-- Key lemma for Mahler's theorem: for `f` a continuous function on `ℤ_[p]`, the sequence
+`n ↦ Δ^[n] f 0` tends to 0. See `PadicInt.fwdDiff_iter_le_of_forall_le` for an explicit
+estimate of the decay rate. -/
+lemma fwdDiff_tendsto_zero (f : C(ℤ_[p], E)) : Tendsto (Δ_[1]^[·] f 0) atTop (𝓝 0) := by
+  -- first extract an `s`
+  refine NormedAddCommGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)
+  have : Tendsto (fun s ↦ ‖f‖ / p ^ s) _ _ := tendsto_const_nhds.div_atTop
+    (tendsto_pow_atTop_atTop_of_one_lt (mod_cast hp.out.one_lt))
+  obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists
+  refine .mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)
+  -- use uniform continuity to find `t`
+  obtain ⟨t, ht⟩ : ∃ t : ℕ, ∀ x y, ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s := by
+    rcases eq_or_ne f 0 with rfl | hf
+    · -- silly case : f = 0
+      simp
+    have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
+    obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
+    obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
+    exact ⟨t, fun x y hxy ↦  by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩
+  filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm
+  simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)
+
+end norm_fwdDiff
+
+end PadicInt

docs/references.bib

@@ -423,6 +423,19 @@ @Book{            bogachev2007
   url           = {https://doi.org/10.1007/978-3-540-34514-5}
 }
 
+@Article{         bojanic74,
+  author        = {Bojani\'c, Ranko},
+  title         = {A simple proof of {M}ahler's theorem on approximation of
+                  continuous functions of a p-adic variable by polynomials},
+  journal       = {Journal of Number Theory},
+  volume        = {6},
+  pages         = {412-415},
+  year          = {1974},
+  issn          = {0022-314X},
+  doi           = {10.1016/0022-314X(74)90038-9},
+  url           = {https://doi.org/10.1016/0022-314X(74)90038-9}
+}
+
 @Book{            bollobas1986,
   author        = {Bollob\'{a}s, B\'{e}la},
   title         = {Combinatorics: Set Systems, Hypergraphs, Families of