pAdicValTR

Stream: Is there code for X?

[Matthew Ballard]

What do people think about

def adicValTR (p n : ℕ) : ℕ :=
  go 0 p n
where go (k p n : ℕ) : ℕ :=
  if h : 1 < p ∧ 0 < n ∧ n % p = 0 then
    have : n / p < n := by apply Nat.div_lt_self <;> aesop
    go (k+1) p (n / p)
  else
    k

with

@[csimp]
theorem padicValNat_eq_adicValTR : @padicValNat = @adicValTR := by ...

For comparison, before

#eval padicValNat 2 (2^10000) -- hangs

while after it is instantaneous. eval for the tail recursive version starts to struggle at 1000000.

[Kevin Buzzard]

We need more of this stuff :-)

[Matthew Ballard]

I've got a reasonably clean proof of padicVal_eq_adicValTR now.

Another question: where should it go? I wanted this for the Miller-Rabin witness test. Is it reasonable to ask similarly minded people to import Mathlib.NumberTheory.Padics.PadicVal? Or should the definition go higher up the dep tree?

[Matthew Ballard]

!4#5158