-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- Bound for norms of ascending Pochhammer symbols. -/
lemma norm_ascPochhammer_le (k : ℕ) (x : ℤ_[p]) :
    ‖(ascPochhammer ℤ_[p] k).eval x‖ ≤ ‖(k.factorial : ℤ_[p])‖

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Tactic:
refine sub_add_cancel (f x) _ ▸ (IsUltrametricDist.norm_add_le_max _ (f n)).trans (max_le hn ?_)

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖f ↑n‖ ≤ ‖↑k.factorial‖

Proof state:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < ‖↑k.factorial‖
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp

Result:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < ‖↑k.factorial‖
n : ℕ
hn' : dist x ↑n < δ
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Tactic:
have hC : (k.factorial : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr k.factorial_ne_zero

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)

Result:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < ‖↑k.factorial‖
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
⊢ ‖Polynomial.eval x (ascPochhammer ℤ_[p] k)‖ ≤ ‖↑k.factorial‖

Tactic:
change ‖f x‖ ≤ ‖_‖

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f x - f n‖ ≤ ‖(k.factorial : ℤ_[p])‖ := by
  obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)
  obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp
  simpa only [← dist_eq_norm_sub'] using ⟨n, (hδ (dist_comm x n ▸ hn')).le⟩

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖↑k.factorial‖ * ‖↑(Ring.multichoose n k)‖ ≤ ‖↑k.factorial‖

Tactic:
exact mul_le_of_le_one_right (norm_nonneg _) (norm_le_one _)

Result:
no goals

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
simp_rw [f, ← ascPochhammer_eval_cast, Polynomial.eval_eq_smeval,
  ← Ring.factorial_nsmul_multichoose_eq_ascPochhammer, smul_eq_mul, Nat.cast_mul, norm_mul]

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖↑k.factorial‖ * ‖↑(Ring.multichoose n k)‖ ≤ ‖↑k.factorial‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Tactic:
have hf : ContinuousAt f x := Polynomial.continuousAt _

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
⊢ ‖f x‖ ≤ ‖↑k.factorial‖

Proof state:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
δ : ℝ
hδp : δ > 0
hδ : ∀ ⦃x_1 : ℤ_[p]⦄, dist x_1 x < δ → dist (f x_1) (f x) < ‖↑k.factorial‖
n : ℕ
hn' : dist x ↑n < δ
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
simpa only [← dist_eq_norm_sub'] using ⟨n, (hδ (dist_comm x n ▸ hn')).le⟩

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
⊢ ‖Polynomial.eval x (ascPochhammer ℤ_[p] k)‖ ≤ ‖↑k.factorial‖

Tactic:
let f := (ascPochhammer ℤ_[p] k).eval

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun a => Polynomial.eval a (ascPochhammer ℤ_[p] k)
⊢ ‖Polynomial.eval x (ascPochhammer ℤ_[p] k)‖ ≤ ‖↑k.factorial‖