Finset of tuples with a given product

Stream: maths

[Arend Mellendijk]

I've gradually been working to extract out results from my work on the Selberg sieve to be added to mathlib. For one important bound I use the fact that the number of ways to write a squarefree natural number $n$ as a product of $k$ naturals is $k^{\omega(n)}$.

The proof is currently far too long, and I think cleaning it up would be a good excuse to develop some API around the Finset of k-tuples with a fixed product, as a generalisation of docs#Nat.divisors and docs#Nat.divisorsAntidiagonal. Something like

def tuplesWithProd {ι : Type _} [Fintype ι] [DecidableEq ι] (d : ℕ) : Finset (ι → ℕ) :=
    (Fintype.piFinset fun _ : ι => d.divisors).filter fun s => ∏ i, s i = d

There's also a connection to docs#Nat.ArithmeticFunction, since the Dirichlet convolution of multiple functions can be expressed as a sum over this set.

Does this sound reasonable? And does anyone have a better name than tuplesWithProd ?

[Eric Wieser]

docs#Finset.Nat.antidiagonalTuple is close, but for sums instead of products

[Eric Wieser]

I would guess you can implement it in very similar way

[Arend Mellendijk]

That definition does look like it's written with computational performance in mind. I doubt that part would transfer over very well since 'number of prime factors' is much slower to recurse on, but the API is probably a good reference.

[Eric Wieser]

Yes, computational performance was certainly a consideration there, as powersets blow up very quickly!

[Yaël Dillies]

@Arend Mellendijk, we have a very similar construction in https://github.com/YaelDillies/LeanAPAP/blob/master/src/prereqs/cut.lean

[Eric Wieser]

Your cut should follow by composing finset.nat.antidiagonal_tuple with trunc_equiv_fin, right?

[Antoine Chambert-Loir]

This week, I also extended @Bhavik Mehta 's initial definition of tuples to arbitrary canonically_ordered_add_monoid, because we needed it for finsupp Types, but — unfortunately — this does not take multiplicative monoids into account.

[Bhavik Mehta]

Might it be feasible to make a (generalised) definition along Antoine's line for canonically_ordered_monoid, which would be appropriately multiplicative (I think?), then to_additive to recover the Antoine's version and the version in archive and LeanAPAP

[Arend Mellendijk]

I don't think nat is a canonically_ordered_monoid though? Because of 0.

[Arend Mellendijk]

Maybe nat under divisibility would work, but you'd still have to worry about finiteness surrounding 0

[Antoine Chambert-Loir]

The problem is that it is not locally finite. Set.Iic 0 is infinite, but all set.Iio n are finite…

[Eric Wieser]

docs#PNat ?

[Arend Mellendijk]

That might make the generalisation work, but I imagine we'd still want some specific API phrased around Nat just so it interacts nicely with the rest of the library.

[Antoine Chambert-Loir]

Probably, antidiagonal n (or for tuples) would work on the subtype { n // Set.Iic n } is finite.

[Arend Mellendijk]

What if you just do what docs#Nat.divisorsAntidiagonal does and set antidiagonal nto be empty if Set.Iic n is infinite?

[Arend Mellendijk]

I'd be worried that's too annoying to work with in general only works out for Nat because there's only one exception

[Antoine Chambert-Loir]

That would be equally fine — and consistent with Lean's philosophy that we want complete functions, with a perfectly reasonable output, actually consistent with Nat.card.