finite product of infinite sums

Stream: Is there code for X?

[Arend Mellendijk]

Do we have a version of docs#tsum_mul_tsum_of_summable_norm for finite products.

My use case is (roughly) to show $\prod_{p\mid n}\frac{1/p}{1-1/p}=\sum_{rad(m)=rad(n)} \frac{1}{m}$. For my application I only need a bound on this product, so I have a workaround of bounding $\frac{1/p}{1-1/p}$ by a finite sum, but I suspect the infinite case will end up having a nicer proof.

[Kevin Buzzard]

If you only have a finite product you should be using docs#Finset.prod rather than tprod and we have a wealth of lemmas for that.

[Arend Mellendijk]

I am! Maybe I should clarify that I expand $\frac{1/p}{1-1/p} = \sum_{m\ge 1} \frac{1}{p^m}$. I'm looking for a lemma about a Finset.prod of a tsum.

[Kevin Buzzard]

Can you ask your question in lean by writing a #mwe with a sorry in ? This is by far the most efficient way of asking such a question.

[Anatole Dedecker]

I haven’t searched extensively, but it’s likely than we don’t have this lemma. Shouldn’t be too hard to add though.

[Arend Mellendijk]

Kevin Buzzard zei:

Can you ask your question in lean by writing a #mwe with a sorry in ? This is by far the most efficient way of asking such a question.

Something like this, though the assumptions might be off a little.

import Mathlib.Analysis.Normed.Field.InfiniteSum
import Mathlib.Analysis.Normed.Group.Basic

open BigOperators Finset

theorem prod_tsum_of_summable_norm {R : Type u_1} {ι : Type u_2} {α : ι → Type u_3}  {s : Finset ι} [inst : NormedCommRing R]
  [inst : CompleteSpace R] {f : (i:ι) → α i → R} (hf : ∀ i, Summable fun x => ‖f i x‖) :
    Summable fun (x : (i:s) → α i) => ‖∏ i in s.attach, f i (x i)‖  := by := sorry

[Anatole Dedecker]

You should add imports to the #mwe so that everything compiles :wink:

[Arend Mellendijk]

Anatole Dedecker zei:

I haven’t searched extensively, but it’s likely than we don’t have this lemma. Shouldn’t be too hard to add though.

But yeah, it should just follow by induction.

[Anatole Dedecker]

Induction-ing your way back to Prods is probably not the best way to deal with this, going from iterated binary product to Pi types will likely makes things more complicated

[Anatole Dedecker]

The cleanest way to do that, which will require quite a bit of work, would be to make a "finite product" API parallel to the "binary product" one, starting with docs#HasSum.mul_eq. We want these result anyway.

[Anatole Dedecker]

But I realize this does not fully solve the problem, and we can't avoid any induction at this first step. That said, I still think the inductive argument will be cleaner if you do not try to get back to an actual Prod type.

[Anatole Dedecker]

Do we have any version of the Fubini theorem (for measures/infinte sums/finite sums, I just want an example) for n-ary products?

[Arend Mellendijk]

docs#Finset.prod_sum ?

[Anatole Dedecker]

Indeed, thanks!

[Arend Mellendijk]

I haven't looked at it very closely, but maybe I should've stated the theorem in terms of Finset.pi rather than pi types.

[Anatole Dedecker]

That doesn't work: docs#Finset.pi is the product of finsets as a finset, but the point is you want to sum over an infinite type.

[Arend Mellendijk]

I repeat my disclaimer.
Also I haven't thought through all the consequences, but my guess would be that if you had an equivalence

import Mathlib.Data.Finset.Basic
open Finset

def insert_pi_equiv {ι : Type _} [DecidableEq ι] (α : ι → Type _) (s : Finset ι) (j : ι) (hj : j ∉ s) :
  ((i : (insert j s:Finset ι)) → α i) ≃ (α j × ((i : s) → α i)) := sorry

the inductive argument wouldn't be too bad. Maybe you'd run into trouble with subtypes, but tsum and Summable seem to interact very well with equivalences.

[Anatole Dedecker]

Yes for sure you can make it work. I was thinking there has to be a clever way to avoid it, but since we have to pi option of docs#HasSum.prod_fiberwise I'm getting pretty sure we actually need to get back to binary products.

[Anatole Dedecker]

As to how to build the desired bijection, you can have a look at docs#Equiv.Set.insert and combine it with docs#Equiv.sumArrowEquivProdArrow

[Alex Kontorovich]

There's a general principle that's quite useful in a lot of elementary number theory: if $f$ is multiplicative and supported on square-free numbers, then $\prod_{p\mid n}\left(1+f(p)\right) = \sum_{d\mid n}f(d)$. I think it would be useful to develop API for this, if it doesn't exist already. (Or you could just ask that $f$ be multiplicative, and then restrict that identity to $n$ which are square-free...)

[Arend Mellendijk]

I do have this result in my project, but there's one snag that arithmetic functions are defined to be 0 at 0, so products of that form aren't naturally arithmetic functions.

[Arend Mellendijk]

You could of course just state it without making it an arithmetic function, and that's fine, but it would still be nice to be able to state the fact that $\prod_{p\mid n} f(p)$ is multiplicative for all $f$...

[Alex Kontorovich]

Arend Mellendijk said:

I do have this result in my project, but there's one snag that arithmetic functions are defined to be 0 at 0, so products of that form aren't naturally arithmetic functions.

Perhaps you're in luck: 1/0 is defined to be 0...?

[Arend Mellendijk]

Sadly Nat.factors 0 = [] and the empty product is one

[Alex Kontorovich]

Argh, right. Yeah, the API will be quite annoying. Unless someone invests in API for $\N_+:=\{n : \N // n \neq 0\}$, which perhaps is better for these applications anyway?...

[Arend Mellendijk]

here's what it would look like if you make that product into an arithmetic function, by the way.

[Arend Mellendijk]

Either way you'd have to write a wrapper around that product to make it into an arithmetic function

[Arend Mellendijk]

That said if you're not too invested in that product being an arithmetic function, I was going to PR that result quite soon, I've just been blocked by #5798

[Kevin Buzzard]

We have docs#PNat and they are used when developing a theory of cyclotomic fields, because (similar to multiplicative functions) nobody could work out any kind of sensible answer to the question "what are the 0th roots of unity?".

Another possibility, which I am coming round to, is that we have a docs#NeZero typeclass which you can just attach to a natural number $n$ and now let typeclass inference do the work of checking that a product of nonzero numbers is nonzero etc.

[Ruben Van de Velde]

What API for docs#PNat is missing?

[Kevin Buzzard]

Do ring and linarith work on it?

[Kevin Buzzard]

import Mathlib.Data.PNat.Basic
import Mathlib.Tactic

example (a b : PNat) : a + b = b + a := by ring -- nope
example (a b c : PNat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by linarith -- nope

On the other hand do goals come up which need these tactics, or is it all about divisibility and products? The positive naturals are a free abelian monoid on the primes and so perhaps the 1 and multiplication are far more important than addition or inequalities.

[Arend Mellendijk]

(deleted)

[Eric Rodriguez]

I've definitely run into weird arithmeticy goals with pnat

[Arend Mellendijk]

To be clear, the biggest thing I've run into with ArithmeticFunction is that I can't just state IsMultiplicative fun n => ∏ p in n.factors.toFinset, f p because ArithmeticFunction is a type synonym for a zero-hom. By itself that isn't a massive problem, but then if you choose to define prodDistinctFactors f : ArithmeticFunction R, then you also want to phrase Alex's statement in terms of that new function, which is just quite ugly.

[Arend Mellendijk]

Kevin Buzzard said

On the other hand do goals come up which need these tactics, or is it all about divisibility and products?

If you're sifting out primes less than y, inequalities do come up.

[Arend Mellendijk]

And in general a big thing about sieves is that they can get you to additive statements about the primes, so thinking about PNat as a monoid isn't very helpful there.

[Kevin Buzzard]

The multiplicative function thing: you just send 0 to 0 in the definition (if x = 0 then 0 else actual definition), and then you make API using if_neg which means that whatever approach you use for positive naturals (PNat or NeZero) you'll never notice the "if" is there. The absence of ring and linarith is a worry -- you might want to ping an expert like @Mario Carneiro to ask whether ring or linarith are going to work on PNat any time soon -- and if the answer is "no I've got a standard library to manage" then I would go with NeZero and I suspect things will be fine.

[Arend Mellendijk]

Maybe the better objection to PNat is that there are a lot of sums over Nat.divisors n, so you would either have to duplicate all that api for PNat or write down a lot of ne_zero_of_mem_divisors

[Anatole Dedecker]

Well morally Nat.divisors should be for PNat anyway, right?

[Anatole Dedecker]

Ultimately the ring you are interested in is MonoidAlgebra Complex PNat, is that right?

[Anatole Dedecker]

docs#MonoidAlgebra

[Anatole Dedecker]

Ah no sorry because you don’t want restriction on the support :face_palm:

[Alex Kontorovich]

Arend Mellendijk said:

If you're sifting out primes less than y, inequalities do come up.

Oh you're doing the Selberg sieve, very nice! I'm not sure which exposition you're following, but in case you're interested, here is the treatment I prefer (written for Brun's theorem, that the sum of reciprocal twin primes converges, but it's practically the general setting...): https://sites.math.rutgers.edu/~alexk/files/BrunSelberg.pdf

[Arend Mellendijk]

Thanks! My original plan was actually to formalise Brun's theorem. I mostly followed Heath-Brown's exposition (https://arxiv.org/abs/math/0209360) with Koukoulopoulos' book as a reference, because they both give a general statement in elementary terms.

[Mario Carneiro]

you might want to ping an expert like Mario Carneiro to ask whether ring or linarith are going to work on PNat any time soon -- and if the answer is "no I've got a standard library to manage"

It's "no, there are some technical issues with making it work or else it would have been done in the initial version"

[Mario Carneiro]

the short version is that it's not a semiring so most of the lemmas don't apply

[Mario Carneiro]

TBH I'm surprised mathlib hasn't invented a quasi-positive-semiring or something for this yet

[Alex Kontorovich]

Arend Mellendijk said:

Thanks! My original plan was actually to formalise Brun's theorem. I mostly followed Heath-Brown's exposition (https://arxiv.org/abs/math/0209360) with Koukoulopoulos' book as a reference, because they both give a general statement in elementary terms.

Will you do the Fundamental Theorem of Sieve Theory? I.e. Iwaniec's theorem, which for bizarre historical reasons is termed the "Rosser sieve" in the literature... (eventually Henryk was so fed up with this, he started calling it the "Beta Sieve"...)

[Kevin Buzzard]

Mario Carneiro said:

TBH I'm surprised mathlib hasn't invented a quasi-positive-semiring or something for this yet

Yeah we need toadditive on NonUnital stuff to make NonZerotalSemiring :-)

[Arend Mellendijk]

Alex Kontorovich said:

There's a general principle that's quite useful in a lot of elementary number theory: if $f$ is multiplicative and supported on square-free numbers, then $\prod_{p\mid n}\left(1+f(p)\right) = \sum_{d\mid n}f(d)$. I think it would be useful to develop API for this, if it doesn't exist already. (Or you could just ask that $f$ be multiplicative, and then restrict that identity to $n$ which are square-free...)

This is addressed in #6662 (in the second form, since I found it easier to work with completely multiplicative functions in my application)