p-adic metric in terms of p-adic norm

Stream: new members

[Giulio Caflisch]

Hello everyone. I'm kind of new to lean and I wanted to ask following question:

I'm working on some small theorems to gain familiarity with analysis and p-adic numbers in Lean 4.
I want to prove the dummy lemma stating p^k tends to zero in the p-adic metric.
I wrote the following code:

import Mathlib

open Nat

variable (p : ℕ) [Fact (Nat.Prime p)]

noncomputable def Padic.prime_powers : ℕ → ℚ_[p] :=
  fun k ↦ (p : ℚ_[p])^k

noncomputable def log_base (b x : ℝ) : ℝ :=
  Real.log x / Real.log b

theorem Padic.prime_powers_tends_to_zero :
    Filter.Tendsto (Padic.prime_powers p) Filter.atTop (nhds (0 : ℚ_[p])) := by
  rw [Metric.tendsto_atTop]
  unfold Padic.prime_powers
  intros ε hε
  let N := Nat.floor (- log_base p ε)
  use N
  intros n hn
  sorry

But somehow I cannot find a Theorem that works for me rewriting following goal

Dist.dist (↑p ^ n) 0 < ε

into its equivalent form involving the norm for metric spaces induced by a norm.

How can I do this?

Thanks in advance for your help!

[Filippo A. E. Nuccio]

Well, docs#dist_eq_norm works, so you can do rw [dist_eq_norm] to do one more step.

[Giulio Caflisch]

Thanks a lot, I don't know how I missed it

[Johan Commelin]

@Giulio Caflisch Do you know about rw?. It is a tactic that searches for useful rewrite lemmas. Near the top of its list of answers is

  rw [@_root_.dist_zero_right]

[Giulio Caflisch]

I know about rw? and simp?. I asked about the more general conversion from distance to norm of difference since I need it in another theorem where the distance is not with respect to 0 and there rw? did not answer anything useful at all.

[Johan Commelin]

Oh, that's unfortunate.

[Johan Commelin]

@loogle Dist.dist ?x ?y < ?ε ↔ ‖?x - ?y‖ < ?ε

[loogle]

:shrug: nothing found

[Johan Commelin]

Hmmmz... That's sad

[Johan Commelin]

Ooh, I'm being silly

[Johan Commelin]

@loogle Dist.dist ?x ?y = ‖?x - ?y‖

[loogle]

:search: dist_eq_norm, dist_eq_norm_sub, and 27 more

[Johan Commelin]

@Giulio Caflisch Voila: loogle is your friend