Theorems · Theorem · number theory

PadicInt.fwdDiff_iter_le_of_forall_le

∀ {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)} {s t : ℕ},
  (∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s) →
    ∀ (n : ℕ), ‖(fwdDiff 1)^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

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.

Defined in

Mathlib.NumberTheory.Padics.MahlerBasis

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupModuleIsBoundedSMulIsUltrametricDist