Theorems · Theorem · number theory

PadicInt.mahlerSeries_apply_nat

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E},
  Filter.Tendsto a Filter.atTop (nhds 0) →
    ∀ {m n : ℕ}, m ≤ n → (PadicInt.mahlerSeries a) ↑m = ∑ i ∈ Finset.range (n + 1), m.choose i • a i

The value of a Mahler series at a natural number n is given by the finite sum of the first m terms, for any n ≤ m.

Defined in

Mathlib.NumberTheory.Padics.MahlerBasis

Cited by

3 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupModuleIsBoundedSMulIsUltrametricDistCompleteSpace