Sum of reciprocal powers over Z^n

Stream: Is there code for X?

[David Loeffler]

Does Mathlib have a proof that for some (equivalently any) norm on $\mathbb{R}^n$, the sum $\sum_{v \in \mathbb{Z}^n} 1/\|v\|^p$ converges iff p > n? The n = 1 case is docs#Real.summable_nat_rpow_inv; the n = 2 case has just come up in a PR I'm reviewing.

[Yaël Dillies]

Sounds like @Chris Birkbeck's stuff

[Chris Birkbeck]

It is indeed. David noticed it can be stated in terms of a norm which is quite neat!

[Chris Birkbeck]

David Loeffler said:

Does Mathlib have a proof that for some (equivalently any) norm on $\mathbb{R}^n$, the sum $\sum_{v \in \mathbb{Z}^n} 1/\|v\|^p$ converges iff p > n? The n = 1 case is docs#Real.summable_nat_rpow_inv; the n = 2 case has just come up in a PR I'm reviewing.

I've not seen such a result, but I could be wrong.

[David Loeffler]

@Xavier Roblot – is this something we have, and if not, is it something you would find useful? I know you've worked a lot on lattices in R^n.

[Xavier Roblot]

No, I don't have this kind of statement. What I have is something like this:

variable (L : AddSubgroup (ι → ℝ)) [DiscreteTopology L] [IsZlattice ℝ L]

theorem tendsto_card_div_pow (b : Basis ι ℤ L) {s : Set (ι → ℝ)} (hs₁ : IsBounded s)
    (hs₂ : MeasurableSet s) :
    Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set (ι → ℝ)) : ℝ) / n ^ card ι)
      atTop (𝓝 ((volume s).toReal / covolume L)) := by

`Well, I guess I may have the tools to prove the result you want but I am still missing the fact that the characteristic function of a bounded set with zero measure frontier is Riemann integrable (BTW, the corresponding hypothesis is missing in the above statement).

[Xavier Roblot]

Wait, I also have this

variable (s : Set (ι → ℝ)) (F : (ι → ℝ) → ℝ) (hF : Continuous F) (hs₁ : Bornology.IsBounded s)
  (hs₂ : MeasurableSet s)

local notation "L" => span ℤ (Set.range (Pi.basisFun ℝ ι))

theorem tendsto_tsum_div_pow :
    Tendsto (fun n : ℕ ↦ (∑' x : ↑(s ∩ (n:ℝ)⁻¹ • L), F x) / n ^ card ι)
      atTop (nhds (∫ x in s, F x)) := by

which should be closer to what to you want.

Still, the same piece as above is missing for the proof of this result.

[Antoine Chambert-Loir]

Since you can take the norm given by supremum of coordinates, this should be much easier.

[Antoine Chambert-Loir]

Mathematically, one can prove that result for the sum over $\mathbf N^n$.
The number of elements $x\in\mathbf N^n$ such that $2^{k-1}<\| x\|_\infty\leq 2^k$ is equal to $(1+2^k)^n-(1+2^{k-1})^n$ which is of the order of $2^{kn}$ (with above and below constants). On each corona, $1/\|x\|_\infty^p$ is of the order of $2^{-pk}$ (with above and below constants). So the result is equivalent to the summability of $2^{(n-p)k}$ for all $k\in\mathbf N$$, a geometric series.

[David Loeffler]

Sure, the proof is not difficult (which is why I posted here, not in #maths). Antoine's "corona" proof (:microbe:?) is pretty much the proof we already have for k = 1. For general k one can also directly count the number of vectors of length exactly n and show it is bounded above + below by multiples of n ^ {k - 1}, then quote the n = 1 case; this is the proof that Chris B formalised for k = 2. But I just wanted to check if the exact result was already here in mathlib.

[Xavier Roblot]

BTW, sorry for unhelpful answers above. I am afraid I misread your question :sweat_smile:

[David Loeffler]

Xavier Roblot said:

BTW, sorry for unhelpful answers above. I am afraid I misread your question :sweat_smile:

No problem. I think your answer would be exactly the right one for a slightly more refined question, studying the asymptotics of the sum as s --> card ι. (I haven't done the analysis carefully, but I suspect that there is a simple pole with residue = volume of the unit ball for our chosen norm, or something like that).

[Antoine Chambert-Loir]

(corona also belongs to the vocabulary of astronomy!)

[Vincent Beffara]

The "corona proof" feels a lot like Cauchy condensation, docs#summable_condensed_iff_of_nonneg except done in dimension n.

[David Loeffler]

We could reduce to the one-dimensional condensation test immediately if we had an additional lemma about gathering together terms in a sum: roughly "if g : α → β has finite fibers, then ∑' a : α, f(g a) = ∑' b : β, card (g ⁻¹' {b})• f b". A more precise statement is

lemma hasSum_comp_iff_hasSum_card_nsmul {α β M : Type*}
    [TopologicalSpace M] [AddCommMonoid M]
      (g : α → β) (f : β → M) (hf : ∀ b : β, Set.Finite (g ⁻¹' {b})) (m : M) :
    HasSum (f ∘ g) m ↔ HasSum (fun b : β ↦ card (hf b).toFinset •  f b) m := by
  sorry

This doesn't seem to be in mathlib either, as far as I can see.

[Antoine Chambert-Loir]

I didn't find it neither when I searched for it this morning…