Proving a sum over smooth numbers is summable

Stream: maths

[Gareth Ma]

Hi, I am trying to prove that the sum $S = \sum_{n, p \mid n \implies p < z} n^{-\delta}$ is summable for all $\delta > 0$. This is true because it is equal to $P = \prod_{p < z} \left(1 - p^{-\delta}\right)$ which is a finite product. However, that requires proving $S = P$, which requires $S$ to be summable i.e. there's some circular argument. Am I correct here? Is there an alternative proof?

[Adam Topaz]

You can use docs#HasSum

[Adam Topaz]

Once you prove HasSum ... P with your P, you can use docs#HasSum.summable to show summability.

[Gareth Ma]

Is HasSum S P equivalent to saying $\lim_{N \to \infty}\left(\sum_{n \leq N, p \mid n \implies p < z} n^{-\delta}\right) = P$? Because that seems even harder to prove

[Adam Topaz]

And finally if you want to show that your sum, defined as tsum, is actuall equal to P, you can use docs#HasSum.tsum_eq

[Adam Topaz]

HasSum is defined as saying that the limit of the partial sums over arbitrary larger and larger finite subsets is equal to P. You can look at the definition itself:

def HasSum (f : β → α) (a : α) : Prop :=
  Tendsto (fun s : Finset β => ∑ b in s, f b) atTop (𝓝 a)

[Gareth Ma]

Right

[Gareth Ma]

So should I write as something like

example (z : ℕ) (δ : ℝ) (hδ : 0 < δ) :
    HasSum
      (fun N : ℕ ↦ if smooth z n then 1 / (n : ℝ) ^ δ else 0)
        (∏ p in prime_Ico 1 z, (1 - 1 / (p : ℝ) ^ δ)⁻¹) := by
  sorry

[Adam Topaz]

I don't know what smooth is.

[Gareth Ma]

Oh oops

[Adam Topaz]

or prime_Ico.

[Gareth Ma]

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Interval
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.NumberTheory.Divisors
import Mathlib.NumberTheory.LSeries

open Nat Finset BigOperators Real ArithmeticFunction

def prime_Ico (a b : ℕ) := (Ico a b).filter Nat.Prime

def smooth (z n : ℕ) := ∀ p ∈ n.factors, p < z

instance : ∀ z, DecidablePred (smooth z) := by unfold smooth ; infer_instance

[Gareth Ma]

it's just short hands for the ranges that appear in the definitions

[Reid Barton]

I guess an approach could be to show that the sets $N_k$ of $z$-smooth numbers in which, in addition, each prime appears at most $k$ times are cofinal in all finite subsets of the $z$-smooth numbers (which ought to be enough since the summands are all nonnegative), and for these subsets $N_k$, we can evaluate the sums as products of truncated geometric series.

[Adam Topaz]

aha I see. yeah you could do that, or you could just use more binders in the sum/product and avoid making these new definitions.

[Gareth Ma]

Reid Barton said:

I guess an approach could be to show that the sets $N_k$ of $z$-smooth numbers in which, in addition, each prime appears at most $k$ times are cofinal in all finite subsets of the $z$-smooth numbers (which ought to be enough since the summands are all nonnegative), and for these subsets $N_k$, we can evaluate the sums as products of truncated geometric series.

Oh! That sounds quite possible - I think I proved something like that already. And also $N_k$ is a finite set / sum, so it should be much easier to handle

[Gareth Ma]

Thanks a lot Reid, I think I will try that approach. Thanks Adam as well :)

[Michael Stoll]

@Gareth Ma My Euler product code basically has the equality $P = S$. It is prod_of_tsum_geometric in EulerFactor.lean.

[Gareth Ma]

Yours doesn't work for my use case since $\sum_n n^{-\delta}$ diverges for $0 < \delta \leq 1$?

[Michael Stoll]

I assume one can prove it using weaker assumptions.

[Gareth Ma]

Maybe yeah, but ∑' n, f n is $0$ currently as stated

[Michael Stoll]

Use that the sums in the product on the left converge absolutely to get convergence of the sum (over smooth numbers) on the right. I'll try to come up with something later if you don't beat me to it.

[Gareth Ma]

I see. But I think I will try to prove it myself first. Thanks though

[Michael Stoll]

I now have

lemma hasSum_prod_tsum_primesBelow
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (N : ℕ) :
    Summable (fun m : N.factorsBelow ↦ ‖f m‖) ∧
      HasSum (fun m : N.factorsBelow ↦ f m) (∏ p in N.primesBelow, ∑' (n : ℕ), f (p ^ n))

(I'll push it to my github repo soon, but you don't have to look :smile: )

In the proof, I had two occurrences of exact <term> leading to a time-out, but have := <term>; exact this succeeding quickly. What could be the reason for this?

[Michael Stoll]

BTW, I think I will change factorsBelow to smoothNumbers in my code, as "smooth" is a pretty common name for the relevant property.

[Kevin Buzzard]

exact <term> means "make this term unify so that it has the type we expect"; have := <term>; exact this means "let the term have whatever type it wants to have, and then check that this is defeq to the type we expect"

[Michael Stoll]

Can you elaborate a bit more on the difference this makes?
One of the terms in questions is summable_mul_of_summable_norm hs ih.1, where

hs: Summable fun n ↦ ‖‖f (N ^ n)‖‖
ih: (Summable fun m ↦ ‖‖f ↑m‖‖) ∧ ...
⊢ Summable fun x ↦ ‖f (N ^ x.1)‖ * ‖f ↑x.2‖

and n in hs is a natural number, m in ih is in ↑(smoothNumbers N) (a subtype of Nat), and x in the goal is in ℕ × ↑(smoothNumbers N).
Could it be related to type class resolution and when this happens?

[Michael Stoll]

BTW, this and the goal look pretty identical. However, using set_option pp.all true, there are some differences in the type classes:

      (@SeminormedRing.toPseudoMetricSpace.{u_1} F
        (@NormedRing.toSeminormedRing.{u_1} F
          (@NormedCommRing.toNormedRing.{u_1} F (@NormedField.toNormedCommRing.{u_1} F inst✝¹))))))

vs.

      (@SeminormedAddCommGroup.toPseudoMetricSpace.{u_1} F
        (@NonUnitalSeminormedRing.toSeminormedAddCommGroup.{u_1} F
          (@NonUnitalNormedRing.toNonUnitalSeminormedRing.{u_1} F
            (@NormedRing.toNonUnitalNormedRing.{u_1} F
              (@NormedCommRing.toNormedRing.{u_1} F (@NormedField.toNormedCommRing.{u_1} F inst✝¹))))))))

and

      (@NonUnitalNonAssocRing.toMul.{u_1} F

vs.

      (@NonUnitalNonAssocSemiring.toMul.{u_1} F
        (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u_1} F

which supports my suspicion...

[Michael Stoll]

Is there some easy way to avoid these problems?

[Kevin Buzzard]

So without seeing a #mwe I will conjecture that doing things one way makes the whole algebra heirarchy explode, and doing it the other way doesn't, for reasons which I have never entirely understood and lie deep in the typeclass system. What happens if you set time-out to 0 and then look at the traces in exact <term>?

[Michael Stoll]

Maybe tomorrow; it's getting late, and I have other things to do...

[Michael Stoll]

It appears that convert <term> has the same effect as have := <term>; exact this.

[Scott Morrison]

No, convert does quite a bit more than that (in particular it will use congr internally and give you subgoals for non-matching subexpressions). But it is strictly more powerful than have := <term>; exact this.

[Michael Stoll]

OK (I know that convert is more powerful, geneally speaking); I should have said "in the context above".