-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- 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. -/
lemma fwdDiff_tendsto_zero (f : C(ℤ_[p], E)) : Tendsto (Δ_[1]^[·] f 0) atTop (𝓝 0)

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
ε : ℝ
hε : ε > 0
s : ℕ
this : Tendsto (fun s => ‖0‖ / ↑p ^ s) atTop (𝓝 0)
hs : ‖0‖ / ↑p ^ s < ε
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖0 x - 0 y‖ ≤ ‖0‖ / ↑p ^ s

Tactic:
simp

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
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
t : ℕ
ht : ↑p ^ (-↑t) < δ
x y : ℤ_[p]
hxy : ‖x - y‖ ≤ ↑p ^ (-↑t)
⊢ ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le

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
f : C(ℤ_[p], E)
⊢ Tendsto (fun x => Δ_[1]^[x] (⇑f) 0) atTop (𝓝 0)

Tactic:
refine NormedAddCommGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε

Proof state:
case inr.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
t : ℕ
ht : ↑p ^ (-↑t) < δ
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
exact ⟨t, fun x y hxy ↦  by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
rcases eq_or_ne f 0 with rfl | hf

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
ε : ℝ
hε : ε > 0
s : ℕ
this : Tendsto (fun s => ‖0‖ / ↑p ^ s) atTop (𝓝 0)
hs : ‖0‖ / ↑p ^ s < ε
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖0 x - 0 y‖ ≤ ‖0‖ / ↑p ^ s

case inr
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
t : ℕ
ht : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
m : ℕ
hm : s * p ^ t ≤ m
⊢ ‖Δ_[1]^[m] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)

Result:
no goals

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε

Tactic:
refine .mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Proof state:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
t : ℕ
ht : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
t : ℕ
ht : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
m : ℕ
hm : s * p ^ t ≤ m
⊢ ‖Δ_[1]^[m] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε

Tactic:
have : Tendsto (fun s ↦ ‖f‖ / p ^ s) _ _ := tendsto_const_nhds.div_atTop
  (tendsto_pow_atTop_atTop_of_one_lt (mod_cast hp.out.one_lt))

Result:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s => ‖f‖ / ↑p ^ s) atTop (𝓝 0)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε