Get Finsupp with all factors less than given number?

Stream: new members

[Ilmārs Cīrulis]

Hello!

There's this beautiful thing Nat.factorization. How can I make the function that filters out all divisors bigger than given number and make new ℕ →₀ ℕ?

Smth like this unfinished effort:

def divisors_under_i (i: ℕ): ℕ → ℕ →₀ ℕ := by
  intros n
  refine Finsupp.mk ?_ (λ x => if x ≤ i then n.factorization x else 0) ?_
  . sorry
  . sorry

[Ilmārs Cīrulis]

Thanks in advance!

[Edward van de Meent]

firstly, since you're defining data, using tactics is a bad idea. secondly, Finsupp.filter should allow you to get basically what you want.

[Ruben Van de Velde]

docs#Finsupp.filter

[Ruben Van de Velde]

Edward beat me to it, but I guessed the same name and it seems appropriate

[Ilmārs Cīrulis]

Why are tactics bad idea (in this case)?

I'm sure that what the tactics have made in this case, is fun n => Finsupp.mk _ (fun x => blabla) _.

[Ilmārs Cīrulis]

#print divisors_under_i confirmed this

[Ilmārs Cīrulis]

If that's really necessary, I can avoid tactics, sure.

[Ruben Van de Velde]

Yeah, intro, refine, exact are all fine

[Ruben Van de Velde]

It's just a bit of an orange flag, because using more complex tactics in the definition makes it harder to prove things about it

[Ilmārs Cīrulis]

Ok, it seems I have finished it. Thank you!

import Mathlib

def divisors_under_i (i n: ℕ): ℕ →₀ ℕ :=
  Finsupp.mk
   (n.factorization.support.filter (λ x => x ≤ i))
   (fun x => if x ≤ i then n.factorization x else 0)
   (by simp; intros a; constructor <;> simp
       . intros H1 H2 H3 H4
         refine ⟨H4, λ H5 => ?_⟩
         rw [Nat.Prime.dvd_iff_one_le_factorization H1 H3, H5] at H2
         exact Nat.not_succ_le_zero 0 H2
       . intros H1 H2
         rw [Nat.factorization_eq_zero_iff] at H2
         simp at H2
         refine ⟨H2, H1⟩
   )

[Edward van de Meent]

how about

def divisors_under_i (i n: ℕ): ℕ →₀ ℕ := n.factorization.filter (fun p => p ≤ i)

[Ruben Van de Velde]

:snail:

[Edward van de Meent]

i suspect this will give better api

[Ilmārs Cīrulis]

Yes, this looks like 100 times more reasonable