Theorems · Theorem · number theory

PadicInt.fwdDiff_tendsto_zero

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] (f : C(ℤ_[p], E)),
  Filter.Tendsto (fun x => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop (nhds 0)

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.

Defined in

Mathlib.NumberTheory.Padics.MahlerBasis

Cited by

2 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactNormedAddCommGroupModuleIsBoundedSMulIsUltrametricDist