Outstanding Tasks, V4

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

Outstanding Tasks V4

For V3, click here.

Here’s a set of targets:

1. MeasureTheory.set_integral_integral_swap is a version of MeasureTheory.integral_integral_swap for sets. Should be very easy. Done by @Vláďa Sedláček
2. MellinConvolutionTransform I made some partial progress; this should require just a little fluency with change of variables in integrals. Done by @Vláďa Sedláček
3. MellinOfPsi This should just be one application of integration by parts, and trivial estimation. Progress by @Vláďa Sedláček
4. Smooth1Properties_below The smoothed indicator function is exactly equal to 1 for $x<1-c \epsilon$.
5. Smooth1Properties_above Same except that the integral is zero if $x>1+c\epsilon$. Done by @Vláďa Sedláček

And continuing on the Fourier side:

6. Decay bounds This should be a straightforward integration by parts (the constant C is explicit, as in the proof). Done by @Vincent Beffara
7. Limiting Fourier Identity This should also be straightforward - combine the two Fourier identities already proven, and invoke dominated convergence using the decay bound. Done by @Vincent Beffara
8. Limiting corollary Immediate from previous identity and the Riemann-Lebesgue lemma
9. Extension to Schwartz class This one is trickier: one wants to extend the identity in the previous corollary from C^2_c functions to Schwartz functions by applying smooth cutoffs (using the smooth Urysohn lemma) and take limits. There will be a moderate amount of estimation of error terms that needs to be done.

Thanks!

[Vláďa Sedláček]

1. is done.

[Vláďa Sedláček]

I've made some progress with 2., but there are two sorries from measure theory that I cannot seem to fill. I'll try moving on to other targets next week.

[llllvvuu]

docs#MeasureTheory.integral_comp_mul_left_Ioi could be helpful (actually, that statement could be improved, it doesn't need the abs).

It may close your proof since it does not require any integrability assumption.

[Vláďa Sedláček]

Thanks, that's exactly what I needed! That finishes 2.

[Alex Kontorovich]

Sorry Vlada, it gave me a merge conflict, and I thought I could handle it myself, but ended up breaking it... :(

[Vláďa Sedláček]

No worries, that was just because of the uncurryfication change (I worked with the old version), but I fixed it now.

[Vincent Beffara]

Having a look at 6, do we have this somewhere already?

lemma decay_bounds_aux3 {ψ : ℝ → ℂ} (h1 : ContDiff ℝ 1 ψ) (h2 : HasCompactSupport ψ) {u : ℝ} :
    𝓕 (deriv ψ) u = 2 * π * I * u * 𝓕 ψ u := by

"This should be a straightforward integration by parts"

[Alex Kontorovich]

Yes we do! See #9773

[Alex Kontorovich]

In particular, docs#hasDerivAt_fourierIntegral should be what you want

[Vincent Beffara]

Not exactly, this is about the derivative of the Fourier transform, not the Fourier transform of the derivative, but it helps, thanks!

[Alex Kontorovich]

I read too quickly... :)

[Vincent Beffara]

Here https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/104 up to an integration by parts lemma which will be a consequence of #10099

From here to decay bounds should be mostly painless, I will give it a go later...

[Vincent Beffara]

decay_bounds is almost done, the only remaining bits are these:

  let f (t : ℝ) := (ψ t - 1 / (4 * ↑π ^ 2) * deriv^[2] ψ t) * ↑(fourierChar (Multiplicative.ofAdd (-t * u)))
  let g (t : ℝ) := A * (1 + 1 / (4 * π ^ 2)) / (1 + t ^ 2)
  have l4 (t : ℝ) : ‖f t‖ ≤ g t := by sorry
  have l5 : Integrable g := sorry

[Ruben Van de Velde]

import Mathlib
open Real MeasureTheory
example {A : ℝ} : True := by
  let g (t : ℝ) := A * (1 + 1 / (4 * π ^ 2)) / (1 + t ^ 2)
  have l5 : Integrable g := by
    unfold_let
    simp_rw [div_eq_mul_inv]
    apply Integrable.const_mul
    apply integrable_inv_one_add_sq
  trivial

[Vincent Beffara]

decay_bounds is sorry-free in the PR above, up to the lemma about integration by parts for compactly supported functions

[Ian Jauslin]

I added details to the blueprint for the proofs of 4,5. In case anyone wants to take a jab at formalizing them

[Vláďa Sedláček]

I've made some progress with 3. (MellinOfPsi) and 5. (Smooth1Properties_above).

[Vincent Beffara]

Vincent Beffara said:

decay_bounds is sorry-free in the PR above, up to the lemma about integration by parts for compactly supported functions

I ended up proving the necessary integration by parts lemmas ...

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/109

[Vincent Beffara]

Some progress on 7. (limiting_fourier)

[Vláďa Sedláček]

4. and 5. are done (modulo a few basic properties in an estimation lemma).

[Vincent Beffara]

Progress on 7. is slower than I thought it would be, because I feel like I have to prove a lot of basic techniques that I did not find in Mathlib, like this:

lemma dirichlet_test {a b A : ℕ → ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hA : 0 ≤ A) (hAa : ∀ n, a n = A (n + 1) - A n)
    (hAb : BoundedAtFilter atTop (fun n ↦ A (n + 1) * b n)) (hbb : Antitone b)
    (h : Summable (fun n ↦ A (n + 1) * (b n - b (n + 1)))) :
    Summable (fun n => a n * b n) := by

I also added a variant of the decay bounds:

lemma decay_bounds_cor {ψ : ℝ → ℂ} (h1 : ContDiff ℝ 2 ψ) (h2 : HasCompactSupport ψ) :
    ∃ C : ℝ, ∀ u, ‖𝓕 ψ u‖ ≤ C / (1 + u ^ 2) := by

(the constant is not explicit because it derives from a compactness argument).

OTOH having to fill in holes in mathlib is one of the main points of having such side-projects anyway :-)

[Michael Stoll]

docs#Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded claims to be "Dirichlet's test for monotone sequences" and docs#Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded for antitone ones.

[Vincent Beffara]

Yes, but we need a more general version here (they use the hypothesis that partial sums of one sequence are bounded, and we have partial sums being O(n)). But the proof is basically the same.

[Vincent Beffara]

Only two self-contained sorries left for 7.:

lemma continuous_FourierIntegral {ψ : ℝ → ℂ} (h1 : Continuous ψ) (h2 : HasCompactSupport ψ) :
    Continuous (𝓕 ψ) := sorry

should follow from standard lemmas about parameterized integrals, I haven't looked yet, and

lemma limiting_fourier_lim1_aux (hcheby : ∃ C, 0 ≤ C ∧ ∀ (x : ℕ), ∑ n in Finset.range x, ‖f n‖ ≤ C * ↑x)
    (hx : 1 ≤ x) (C : ℝ) :
    Summable fun n ↦ ‖f n‖ / ↑n * (C / (1 + (1 / (2 * π) * Real.log (↑n / x)) ^ 2)) := by
  sorry

should follow from summation by parts / Dirichlet test plus comparison with sum of inverse of n * (log n) ^ 2 plus convergence of that.

[Sébastien Gouëzel]

Are you aware of docs#VectorFourier.fourierIntegral_continuous for the continuity?

[Vincent Beffara]

Ah, in fact I hadn't even looked in mathlib for the result yet, I was focussing on other parts of the proof ... Thanks!

[Vincent Beffara]

lemma continuous_FourierIntegral {ψ : ℝ → ℂ} (h1 : Continuous ψ) (h2 : HasCompactSupport ψ) :
    Continuous (𝓕 ψ) :=
  VectorFourier.fourierIntegral_continuous continuous_fourierChar (by exact continuous_mul) <|
    h1.integrable_of_hasCompactSupport h2

[Vincent Beffara]

One sorry left for 7.:

def nnabla {E : Type*} [HSub E E E] (u : ℕ → E) (n : ℕ) : E := u n - u (n + 1)

lemma nnabla_bound {C : ℝ} (hx : 1 ≤ x) :
    nnabla (fun n : ℕ => C / (1 + (Real.log (↑n / x) / (2 * π)) ^ 2) / ↑n) =O[atTop]
    (fun n : ℕ => (n ^ 2 * (Real.log n) ^ 2)⁻¹) := by
  sorry

I haven't yet found a non-painful way to prove such things...

[Terence Tao]

One could set up a bit of API for nnabla to help you. In particular,

nnabla (C • f) = C • (nnabla f)

nnabla (fun n => f n + C) = nnabla f

nnabla (f * g) n = (nnabla f n) * (g n) + (f (n+1)) * (nnabla g n)

nnabla (1/f) n = - (nabla f n) / ((f n) * (f (n+1))

nnabla log =O[atTop] (fun n => 1 / n)

nnabla (fun n => n ) = 1

and the =O[] calculus should get you most of the way there eventually...

[Vincent Beffara]

The main pain points come from lemmas about monotone sequences while here the sequences are only eventually monotone because of trash values at 0, things like this

[Gareth Ma]

Define a shifted sequence then?

[Vincent Beffara]

Gareth Ma said:

Define a shifted sequence then?

Yes, exactly, and show in API that a sequence is summable iff its shift is summable and so on. But, sometimes the amount of shift to be done is not fixed (like e.g. log (n / a) ^ 2 which does appear in the estimates, with variable a, and is only increasing starting at n = a). Nothing unfeasible, but it takes time...

[Michael Stoll]

There is docs#summable_nat_add_iff in case this helps...

[Vincent Beffara]

Task 7. is done at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/111 (700-line PR, mergeable but in dire need of refactoring ...)

[Terence Tao]

Wow, that was surprisingly difficult. What part of the argument was the most challenging to formalize? Are there some gaps in current Mathlib API that need to be filled? (I'm wondering if we should tweak some of the remaining blueprint to avoid whatever obstacles you ended up encountering.)

[Vincent Beffara]

I wish I had a clear answer to that question. A big part of it is that I was discovering the =O[] API along the way, so upon refactoring things will get better. Another part is that I did not pause enough to think about the principled approach of developing the needed API from the ground up. But more generally, there was no precise point in the argument that was really more difficult, it was more about fighting friction all the time.

[Vláďa Sedláček]

Any idea how to prove ↑(MellinConvolution (fun x ↦ if x ≤ 1 then 1 else 0) (DeltaSpike Ψ ε) x) = MellinConvolution (fun x ↦ if x ≤ 1 then 1 else 0) (fun x ↦ ↑(DeltaSpike Ψ ε x)) x? Should be a simple coercion matter, but none of the tactics I tried work.

[Vincent Beffara]

lemma MellinOfSmooth1a (Ψ : ℝ → ℝ)
    {ε : ℝ} (εpos : 0 < ε) {s : ℂ} (hs : 0 < s.re) :
    MellinTransform ((Smooth1 Ψ ε) ·) s = 1 / s * MellinTransform (Ψ ·) (ε * s) := by
  unfold Smooth1
  -- let g := DeltaSpike Ψ ε
  let g: ℝ → ℂ  := fun x ↦ DeltaSpike Ψ ε x
  have : IntegrableOn (Function.uncurry fun x y ↦ (if y ≤ 1 then 1 else 0) *
      g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) := by
    sorry
  have := MellinConvolutionTransform (fun x ↦ if x ≤ 1 then 1 else 0) g s this
  convert this using 1
  · simp [g]
    congr; funext x
    simp [MellinConvolution, DeltaSpike]
    convert integral_ofReal.symm
    push_cast
    congr
    change _ = ofReal' _
    simp [@apply_ite ℝ ℂ]
  · rw [MellinOf1 s hs, MellinOfDeltaSpike Ψ εpos s]

[Vincent Beffara]

No idea why it is so complicated...

[Vláďa Sedláček]

Great, thanks, I was missing integral_ofReal.

[Vincent Beffara]

Task 8. is done (and this time it really was as immediate as the math was indicating :big_smile:)

[Vincent Beffara]

So I started looking at limiting_cor_schwartz and it seems that it is going to take a while. The idea of the proof is clear enough but controlling \psi_{>R} as described via decay_bounds means extending decay_bounds itself to the Schwartz class (which, sure it holds especially with an explicit constant that does not depend on the support). And the extension of that starts with truncation with a smooth cutoff, essentially duplicating a large part of the blueprint for limiting_cor_schwartz.

So it seems that there are two reasonable approaches:

1. Go through the whole file and replace everywhere "compact support" with "Schwarz class" (or something in between like C^2 with fast enough decay of the function and its first two derivatives, so that we do not lose any generality). But perhaps compact support is really fundamental at some step of the existing proof.
2. Build some API around smooth truncation of functions (a part of that may already be in Mathlib somewhere, I did not look seriously yet), and use it to implement the blueprint as it is.

Option 2 is certainly something of more general interest, but it would definitely take (a lot) longer. Any preference?

[Terence Tao]

Hmm, well, compact support is needed in one place: to show that $G(1+it) \psi(t)$ is absolutely integrable (or more precisely, that $G(\sigma+it) \psi(t)$ is dominated by an absolutely integrable function as $\sigma$ approaches 1) in Lemma 4. If $\psi$ were merely required to be Schwartz, then we would need an extra hypothesis that $G$ is of polynomial growth, which is true for our specific application, but makes the Wiener-Ikehara theorem weaker as this is not one of the standard hypotheses of the theorem.

So perhaps what is needed is to perform Approach 1 for the decay bounds lemma (i.e., generalize Lemma 3 to Schwartz functions rather than compactly supported functions), and whatever is needed from approach 2 to then finish the job. To prove the decay bounds lemma for Schwartz functions, I think the main thing that is needed is an integration by parts lemma of the form

$\int_{\bf R} f(x) g'(x)\ dx = - \int_{\bf R} f'(x) g(x)\ dx$
whenever $f, g$ are continuously differentiable, with $fg$ tending to zero at infinity, and $fg'$ and $f'g$ both absolutely integrable. This should be doable by integrating by parts on some finite interval $[-R,R]$ and then sending $R$ to infinity. That should be good enough to obtain the key identity
$(1 + u^2) \hat \psi(u) = \int_{\bf R} (\psi(t) - \frac{1}{4\pi^2} \psi''(t)) e(-tu)\ dt$
for Schwartz $\psi$, which should then give the decay bounds. (The $u$ in the numerator in the blueprint for this formula is a typo.)

[Terence Tao]

Actually, a better way to proceed may be to show that (a) Schwartz functions are preserved under the operation of taking derivatives; (b) If $\psi$ is Schwartz, then Fourier transform of $\psi'$ is $\xi \mapsto 2\pi i \xi \hat \psi(\xi)$, as this will also give the decay bounds; and when combined with (a') Schwartz functions are preserved under the operation of multiplying by $x$, and (b') If $\psi$ is Schwartz, then $\hat \psi$ is differentiable and the Fourier transform of $x \mapsto x \psi(x)$ is $\frac{-1}{2\pi i} \frac{d}{d\xi} \hat \psi$, will also give that the Fourier transform of a Schwartz function is Schwartz, as this will be needed very shortly also. (Claim (a) will still need the integration by parts lemma indicated above, which may still be worth proving as a standalone lemma.)

[llllvvuu]

docs#MeasureTheory.integral_mul_deriv_eq_deriv_mul may help

[Terence Tao]

OK, that does help. So I think the subgoals for limiting_cor_schwarz could be

1. Show that the derivative of a Schwartz function is Schwartz.
2. Show that if $\psi$ is Schwartz, then the Fourier transform of $\psi'$ is $u \mapsto 2\pi i u \hat \psi(u)$ (here we would use docs#MeasureTheory.integral_mul_deriv_eq_deriv_mul and also part 1, as well as the fact that Schwartz functions are absolutely integrable and decay to zero at infinity. )
3. Show that if $\psi$ is Schwartz, then $u \mapsto (1+u^2) \hat \psi(u)$ is the Fourier transform of $\psi - \frac{1}{4\pi^2} \psi''$. (This comes from 1, 2, and linearity of the Fourier transform.)
4. Establish decay_bounds for Schwartz functions (this should be a modification of the existing proof once we have 3.)
5. At this point the blueprint proof of limiting_cor_schwartz will hopefully be straightforward?

[Vincent Beffara]

This feels very doable. 1. is docs#SchwartzMap.derivCLM 2. is decay_bounds_aux3 in Wiener.lean extended from compact support to Schwartz class but compact support is only used in integration by parts so it should be reasonably easy, and the rest feels rather direct.

[David Loeffler]

Terence Tao said:

[...]

2. Show that if $\psi$ is Schwartz, then the Fourier transform of $\psi'$ is $u \mapsto 2\pi i u \hat \psi(u)$ (here we would use docs#MeasureTheory.integral_mul_deriv_eq_deriv_mul and also part 1, as well as the fact that Schwartz functions are absolutely integrable and decay to zero at infinity. )

This is already in mathlib: docs#hasDerivAt_fourierIntegral (under different assumptions, i.e. that $f$ and $f'$ be $L^1$, but it shouldn't be hard to check that these hold for Schwartz functions). EDIT: sorry, this is wrong, I was confusing this with the opposite statement (derivative of the transform, not transform of the derivative) – apologies for the noise!

[Vincent Beffara]

I can prove this:

lemma fourierIntegral_deriv (ψ : SchwartzMap ℝ ℂ) (u : ℝ) : 𝓕 (deriv ψ) u = 2 * π * I * u * 𝓕 ψ u := by

but the proof is awfully ugly, I am rewriting it.

[Vincent Beffara]

BTW, it would definitely make sense to have a result like this under more minimal hypotheses, so that we can apply it both to Schwartz class and to C^2 with compact support, because as it is we will end up with a lot of code duplication. Ditto for the decay bounds, we should state it on W^{2,1} or something.

[Terence Tao]

One set of hypotheses could be: $\psi$ is continuously differentiable, and $\psi$ and $\psi'$ are both absolutely integrable with $\psi$ converging to zero at infinity. Actually, if one wanted to work a bit harder, one could drop the hypothesis of converging to zero at infinity, because the absolute integrability implies convergence to zero along a sequence tending to infinity, which suffices; but then one could not use docs#MeasureTheory.integral_mul_deriv_eq_deriv_mul "out of the box". Then one would be close to the minimal hypotheses given that the Fourier transform in Lean only gives non-junk values for absolutely integrable functions (if I understand the documentation correctly).

[Terence Tao]

David Loeffler said:

Terence Tao said:
This is already in mathlib: docs#hasDerivAt_fourierIntegral (under different assumptions, i.e. that $f$ and $f'$ be $L^1$, but it shouldn't be hard to check that these hold for Schwartz functions). EDIT: sorry, this is wrong, I was confusing this with the opposite statement (derivative of the transform, not transform of the derivative) – apologies for the noise!

No problem - that opposite statement will also come in handy later when we need to show that the Fourier transform of a Schwartz function is Schwartz.

[Vincent Beffara]

Terence Tao said:

One set of hypotheses could be: $\psi$ is continuously differentiable, and $\psi$ and $\psi'$ are both absolutely integrable with $\psi$ converging to zero at infinity. Actually, if one wanted to work a bit harder, one could drop the hypothesis of converging to zero at infinity, because the absolute integrability implies convergence to zero along a sequence tending to infinity, which suffices; but then one could not use docs#MeasureTheory.integral_mul_deriv_eq_deriv_mul "out of the box". Then one would be close to the minimal hypotheses given that the Fourier transform in Lean only gives non-junk values for absolutely integrable functions (if I understand the documentation correctly).

Like this:

theorem fourierIntegral_deriv {f f' : ℝ → ℂ} (h1 : ∀ x, HasDerivAt f (f' x) x) (h2 : Integrable f)
    (h3 : Integrable f') (h4 : Tendsto f (cocompact ℝ) (𝓝 0)) (u : ℝ) :
    𝓕 f' u = 2 * π * I * u * 𝓕 f u := by
  convert_to ∫ v, e u v * f' v = 2 * ↑π * I * ↑u * ∫ v, e u v * f v
    <;> try { simp [fourierIntegral_real_eq] }
  have l1 (x) : HasDerivAt (e u) (-2 * π * u * I * e u x) x := hasDerivAt_e
  have l3 : Integrable (⇑(e u) * f') := fourierIntegral_deriv_aux2 (e u) h3
  have l4 : Integrable (fun x ↦ -2 * π * u * I * e u x * f x) := by
    simpa [mul_assoc] using (fourierIntegral_deriv_aux2 (e u) h2).const_mul (-2 * π * u * I)
  have l7 : Tendsto (⇑(e u) * f) (cocompact ℝ) (𝓝 0) := by
    simpa [tendsto_zero_iff_norm_tendsto_zero] using h4
  have l5 : Tendsto (⇑(e u) * f) atBot (𝓝 0) := l7.mono_left _root_.atBot_le_cocompact
  have l6 : Tendsto (⇑(e u) * f) atTop (𝓝 0) := l7.mono_left _root_.atTop_le_cocompact
  rw [integral_mul_deriv_eq_deriv_mul l1 h1 l3 l4 l5 l6]
  simp [integral_neg, ← integral_mul_left] ; congr ; ext ; ring

theorem fourierIntegral_deriv_schwartz (ψ : 𝓢(ℝ, ℂ)) (u : ℝ) : 𝓕 (deriv ψ) u = 2 * π * I * u * 𝓕 ψ u :=
  fourierIntegral_deriv (fun _ => ψ.differentiableAt.hasDerivAt) ψ.integrable
    (SchwartzMap.derivCLM ℝ ψ).integrable ψ.toZeroAtInfty.zero_at_infty' u

theorem fourierIntegral_deriv_compactSupport {f : ℝ → ℂ} (h1 : ContDiff ℝ 1 f) (h2 : HasCompactSupport f) (u : ℝ) :
    𝓕 (deriv f) u = 2 * π * I * u * 𝓕 f u := by
  have l1 (x) : HasDerivAt f (deriv f x) x := (h1.differentiable le_rfl).differentiableAt.hasDerivAt
  have l2 : Integrable f := h1.continuous.integrable_of_hasCompactSupport h2
  have l3 : Integrable (deriv f) := (h1.continuous_deriv le_rfl).integrable_of_hasCompactSupport h2.deriv
  exact fourierIntegral_deriv l1 l2 l3 h2.is_zero_at_infty u

[David Loeffler]

the Fourier transform in Lean only gives non-junk values for absolutely integrable functions (if I understand the documentation correctly)

That's correct, at least at present. (I think Sebastian Gouezel is working on Fourier transforms of tempered distributions, but it hasn't landed in mathlib yet.)

[Terence Tao]

Hmm, if there is ongoing work to establish Fourier transforms for tempered distributions, then surely that work would also have to show at some point that the (inverse) Fourier transform of a Schwartz function is Schwartz, which we will soon need ourselves...

[Vincent Beffara]

Decay bounds in the Schwartz class here https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/129 :

lemma decay_bounds {ψ : ℝ → ℂ} {A u : ℝ} (h1 : ContDiff ℝ 2 ψ) (h2 : HasCompactSupport ψ)
    (hA : ∀ t, ‖ψ t‖ ≤ A / (1 + t ^ 2)) (hA' : ∀ t, ‖deriv^[2] ψ t‖ ≤ A / (1 + t ^ 2)) :
    ‖𝓕 ψ u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2) := by
  exact decay_bounds_W21 (W21_of_compactSupport h1 h2) hA hA' u

lemma decay_bounds_schwartz (ψ : 𝓢(ℝ, ℂ)) (u : ℝ)
    (hA : ∀ t, ‖ψ t‖ ≤ A / (1 + t ^ 2)) (hA' : ∀ t, ‖deriv^[2] ψ t‖ ≤ A / (1 + t ^ 2)) :
    ‖𝓕 ψ u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2) := by
  exact decay_bounds_W21 (W21_of_schwartz ψ) hA hA' u

At the moment we are not using the exact value for the bound, and the exact shape of the assumption on \psi is not really used either, it is only exploited to show that both \psi and its second derivative are integrable (with a small L^1 norm). Using this as a hypothesis instead would likely simplify the proof of limiting_cor_schwartz because instead of proving such a quantitative bound on the function minus its smooth truncation it seems that only convergence in L^1 of the truncated function would suffice?

[Vincent Beffara]

I refactored it just in case : this is true

lemma decay_bounds_key {f : ℝ → ℂ} (hf : W21 f) (u : ℝ) :
    ‖𝓕 f u‖ ≤ ((∫ v, ‖f v‖) + (4 * π ^ 2)⁻¹ * (∫ v, ‖deriv (deriv f) v‖)) * (1 + u ^ 2)⁻¹

and this is also true

lemma decay_bounds_aux {f : ℝ → ℂ} (hf : AEStronglyMeasurable f volume) (h : ∀ t, ‖f t‖ ≤ A * (1 + t ^ 2)⁻¹) :
    ∫ t, ‖f t‖ ≤ π * A

and this follows

theorem decay_bounds_W21 {f : ℝ → ℂ} (hf : W21 f) (hA : ∀ t, ‖f t‖ ≤ A / (1 + t ^ 2))
    (hA' : ∀ t, ‖deriv (deriv f) t‖ ≤ A / (1 + t ^ 2)) (u) :
    ‖𝓕 f u‖ ≤ (π + 1 / (4 * π)) * A / (1 + u ^ 2)

but this takes a shortcut

lemma decay_bounds_cor {ψ : ℝ → ℂ} (h1 : ContDiff ℝ 2 ψ) (h2 : HasCompactSupport ψ) :
    ∃ C : ℝ, ∀ u, ‖𝓕 ψ u‖ ≤ C / (1 + u ^ 2) := by
  simpa only [div_eq_mul_inv] using ⟨_, decay_bounds_key (W21_of_compactSupport h1 h2)⟩

which is enough for limiting_fourier but not for controlling tails after smooth cutoffs.

[Vincent Beffara]

In fact (∫ v, ‖f v‖) + (4 * π ^ 2)⁻¹ * (∫ v, ‖deriv (deriv f) v‖) is a natural norm on the pseudo-W21 space here, and probably what is needed now is convergence of larger and larger truncations to the function in the corresponding topology.

[Terence Tao]

I like this approach. One could try to show that the functional $\psi \mapsto \limsup_{x \to \infty} | \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi(\frac{1}{2\pi} \log \frac{n}{x} ) - A \int_{-\infty}^\infty \hat \psi(\frac{u}{2\pi})\ du|$ is (a) continuous (in fact Lipschitz) in the Schwartz space equipped with this pseudo-W21 seminorm; (b) vanishes on compactly supported Schwartz functions; and that (c) the compactly supported Schwartz functions are dense in the Schwartz space under this seminorm. Then it should vanish on the entire Schwartz space by some general topological lemma (possibly already in mathlib). One downside of this approach though is that one may have to verify the semi-norm axioms, which could be a little tedious.

[Vincent Beffara]

I just PRed this, which is point (c), to PNT+:

structure trunc (g : ℝ → ℝ) : Prop :=
  h1 : ContDiff ℝ ⊤ g
  h2 : HasCompactSupport g
  h3 : (Set.Icc (-1) (1)).indicator 1 ≤ g
  h4 : g ≤ Set.indicator (Set.Ioo (-2) (2)) 1

theorem W21_approximation {f : ℝ → ℂ} (hf : W21 f) {g : ℝ → ℝ} (hg : trunc g) :
    Tendsto (fun R => W21.norm (fun v => (1 - g (v * R⁻¹)) * f v)) atTop (𝓝 0) := by

[Vincent Beffara]

For this particular result, g being C^2 bounded with bounded first and second derivatives, and equal to 1 in a neighborhood of 0, is enough to get convergence

[Terence Tao]

Great! It looks like we have all the pieces then to get the Schwartz extension.

One observation is that the lim sup functional is itself a seminorm, though I don't know whether that will make things any faster to formalize (it does mean though that continuity will follow once one can show that this seminorm is dominated by the W21 norm, which is what decay_bounds should do).

[Vincent Beffara]

I can prove this

lemma bound_I2 (x : ℝ) (ψ : ℝ → ℂ) (hψ : W21 ψ) :
    ‖∫ u in Set.Ici (-log x), 𝓕 ψ (u / (2 * π))‖ ≤ W21.norm ψ * (2 * π ^ 2) := by

which is fine, and this

lemma bound_I1 (x : ℝ) (hx : 0 < x) (ψ : ℝ → ℂ) (hψ : W21 ψ) (hcheby : cumsum (‖f ·‖) =O[atTop] ((↑) : ℕ → ℝ)) :
    ‖∑' n, f n / n * 𝓕 ψ (1 / (2 * π) * log (n / x))‖ ≤
    W21.norm ψ * ∑' (i : ℕ), ‖f i / i * ((1 + (1 / (2 * π) * Real.log (i / x)) ^ 2)⁻¹ : ℂ)‖ := by

which should also be fine eventually but the bound depends on x so we will likely have to control the sum by an Abel transform again (the way these things are written now higher in the file is using =O[] for fixed x with implicit constants, so it is not enough).

[Terence Tao]

Ugh, I had forgotten about this "routine" asymptotic computation. One could possibly try to perform a dyadic decomposition based on the integer part of Real.log (i/x), use hcheby to bound each component, and then sum up. (One small thing is that it might be convenient to make a lemma that one can replace the atTop filter in hcheby by the ⊤ filter, so that one gets to control the cumsum for all x, not just for suffiicently large x.)

[Vincent Beffara]

I think I would rather use docs#Finset.sum_range_by_parts together with docs#tsum_le_of_sum_range_le to match with the previous domination argument (and indeed, replacing hcheby with a uniform estimate does not affect generality and will simplify everything).

[Vincent Beffara]

(OTOH, this dyadic approach is essentially a quantitative version of docs#summable_condensed_iff_of_nonneg which I used to show summability, so it will certainly come up at some point.)

[Vincent Beffara]

I did not report a lot recently because I was going down a rabbit hole trying to give uniform bounds of derivatives on intervals of the form log (i / x) to log ((i + 1) / x) and failing to fight the system - but I finally realized that you can do the Abel transform, bound the sum of the norms of the f i, and then do the Abel transform backwards. So I now have a technical lemma saying this:

lemma cancel_aux' {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g)
    (hf' : ∀ n, cumsum f n ≤ C * n) (hg' : Antitone g) (n : ℕ) :
    ∑ i in Finset.range n, f i * g i ≤
        C * n * g (n - 1)
      + C * cumsum g (n - 1 - 1 + 1)
      - C * (↑(n - 1 - 1) + 1) * g (n - 1)

Still needs some polishing, but I have hope that the pain is behind me :-)

[Vincent Beffara]

We are lucky that 1 / (2 * \pi) is less than one!

[Vincent Beffara]

Hm, should have finished the polishing before speaking, because the actual bound is like this:

lemma cancel_main {C : ℝ} {f g : ℕ → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g)
    (hf' : ∀ n, cumsum f n ≤ C * n) (hg' : Antitone g) (n : ℕ) (hn : 2 ≤ n) :
    ∑ i in Finset.range n, f i * g i ≤ C * cumsum g n := by

This is very likely to be well known...

[Vincent Beffara]

(And if f 0 = 0 which we have, then it holds for all n.)

[Terence Tao]

Nice lemma! Things like this show up in harmonic analysis, where the Hardy-Littlewood maximal function $Mf(x) := \sup_{r>0} \frac{1}{2r} \int_{x-r}^{x+r} |f(y)|\ dy$ is used to control other averages of $f$ around $x$, such as integrals of $f$ against a radially decreasing function around $x$. I'm not sure that there is a canonical estimate of this form that would be general-purpose enough for Mathlib, though.

[Vincent Beffara]

All right,

lemma bound_sum_log' {C : ℝ} (hf : chebyWith C f) {x : ℝ} (hx : 1 ≤ x) :
    ∑' i, ‖f i‖ / i * (1 + (1 / (2 * π) * log (i / x)) ^ 2)⁻¹ ≤ C * (1 + 2 * π ^ 2) := by

Now to put the pieces together ...

[Vincent Beffara]

And this:

lemma bound_I1' {C : ℝ} (x : ℝ) (hx : 1 ≤ x) (ψ : ℝ → ℂ) (hψ : W21 ψ) (hcheby : chebyWith C f) :
    ‖∑' n, f n / n * 𝓕 ψ (1 / (2 * π) * log (n / x))‖ ≤ W21.norm ψ * C * (1 + 2 * π ^ 2) := by

[Vincent Beffara]

'limiting_cor_schwartz' depends on axioms: [propext, Classical.choice, Quot.sound]

[Terence Tao]

I think that was the hardest step towards the Wiener-Ikehara theorem (and thence to PNT). Hopefully we are in the home stretch now...

[Vincent Beffara]

(Not sure it is relevant for later, but in fact limiting_cor_schwartz works with no modification at all for all W21 functions.)

[Vincent Beffara]

deleted sorry I did not think through this carefully ...

[Vláďa Sedláček]

I have made a lot of progress with MellinCalculus.lean, almost all the relevant proofs are finished. Some remarks:

• I would welcome any help to finish the integrability condition in MellinOfSmooth1a, as I've been stuck on that for quite some time. TLDR is here and I have some doubts about the current approach.
  - DeltaSpikeSupport is done except when x is negative (and the remaining goal is to show that x ^ ε⁻¹ is also negative, which might not even make sense). I also just realized the statement is false (for example x could be negative and ε an even integer. Is there a good way to repair the statement without restricting the definition domain of DeltaSpike to Ioi 0?
  - After heavy refactoring, many proofs are now quite readable, but others would still benefit from a separate API (e.g., a simple partial integration calculation, which currently has over 100 lines) to not break the chain of thought. I'll keep working on that more and I'll appreciate any suggestions.

[Vláďa Sedláček]

MellinOfSmooth1a is done, I found a nice shortcut. Thus MellinCalculus is sorry-free (except for four lemmas which are never used).