-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
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`.
-/
lemma mahlerSeries_apply_nat (ha : Tendsto a atTop (𝓝 0)) {m n : ℕ} (hmn : m ≤ n) :
    mahlerSeries a (m : ℤ_[p]) = ∑ i ∈ range (n + 1), m.choose i • a i

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
⊢ (mahlerSeries a) ↑m = ∑ i ∈ range (n + 1), m.choose i • a i

Tactic:
have aux : Summable fun i ↦ m.choose (i + (n + 1)) • a (i + (n + 1)) := by
  simpa only [h_van, zero_smul] using summable_zero

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
aux : Summable fun i => m.choose (i + (n + 1)) • a (i + (n + 1))
⊢ (mahlerSeries a) ↑m = ∑ i ∈ range (n + 1), m.choose i • a i

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
i : ℕ
⊢ m < i + (n + 1)

Tactic:
omega

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
aux : Summable fun i => m.choose (i + (n + 1)) • a (i + (n + 1))
⊢ (mahlerSeries a) ↑m = ∑ i ∈ range (n + 1), m.choose i • a i

Tactic:
simp only [mahlerSeries_apply ha, mahler_natCast_eq, Nat.cast_smul_eq_nsmul, add_zero,
  ← sum_add_tsum_nat_add' (f := fun i ↦ m.choose i • a i) aux, h_van, zero_smul, tsum_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
⊢ Summable fun i => m.choose (i + (n + 1)) • a (i + (n + 1))

Tactic:
simpa only [h_van, zero_smul] using summable_zero

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
⊢ (mahlerSeries a) ↑m = ∑ i ∈ range (n + 1), m.choose i • a i

Tactic:
have h_van (i) : m.choose (i + (n + 1)) = 0 := Nat.choose_eq_zero_of_lt (by omega)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
m n : ℕ
hmn : m ≤ n
h_van : ∀ (i : ℕ), m.choose (i + (n + 1)) = 0
⊢ (mahlerSeries a) ↑m = ∑ i ∈ range (n + 1), m.choose i • a i