Theorems · Theorem · number theory

PadicInt.hasSum_mahler

• 1000+ list: Mahler's theorem

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [inst_3 : IsUltrametricDist E] [CompleteSpace E] (f : C(ℤ_[p], E)),
  HasSum (fun n => PadicInt.mahlerTerm ((fwdDiff 1)^[n] (⇑f) 0) n) f

Mahler's theorem: for any continuous function f from ℤ_[p] to a p-adic Banach space, the Mahler series with coefficients n ↦ Δ_[1]^[n] f 0 converges to the original function f.

Defined in

Mathlib.NumberTheory.Padics.MahlerBasis

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupModuleIsBoundedSMulIsUltrametricDistCompleteSpace