Outstanding Tasks, V5

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

For V4, click here.

I've refactored the Second Approach (see the new file ZetaBounds), outlining a method that avoids any more complex analytic developments than those we already have (in particular, no Hadamard, not even Jensen). Just using very classical techniques (partial summation), this gives the error term $O(x \exp(-c (\log x)^{1/10})$ (whereas StrongPNT was meant to replace the exponent $1/10$ with $1/2$). I'm thus renaming WeakPNT2 to MediumPNT. This error is basically good enough for just about any application, as it gets a rate that's better than $O(x/\log^C x)$, for any $C>0$. As far as I'm aware (please correct me?), this will be the first time that an error of this quality is formalized. (We'll see if we even want to continue pushing for StrongPNT; we might want to move right on to Dirichlet/Chebotarev... I've temporarily (?) taken the StrongPNT section out of the blueprint, so we can see the dependency graph a bit clearer.) This also means we will no longer need any Selberg upper bound sieving (sorry @Arend Mellendijk!).

With those caveats, here's the next round of targets (I tried to break them into really rather small pieces, so there are a few more than usual):

1. sum_eq_int_deriv This is partial summation. I've already almost (modulo some annoying stuff mixing up uIoo and uIcc in sum_eq_int_deriv_aux2) got it proved on intervals of length at most one (sum_eq_int_deriv_aux), so now it's just a matter of stringing those together. Done by me
2. ZetaSum_aux1 is just an application of partial summation to the power function. Should not be too hard. Done by me
3. ZetaSum_aux1a is an auxiliary function, amounts to applying the triangle inequality inside an integral. Shouldn't be hard. Done by @Paul Nelson
4. ZetaSum_aux2 is taking ZetaSum_aux1 and sending $b\to\infty$. Done by @Heather Macbeth, @Vláďa Sedláček and me
5. ZetaBnd_aux1 is a combination of 3. and 4., namely applying the triangle inequality inside an integral and sending $b\to\infty$. Done by @Heather Macbeth, @Vláďa Sedláček and me
6. Zeta0EqZeta is that the two zeta functions now defined agree on $\Re(s)>0$ (but not necessarily at $s=1$, since we don't know/care what the junk value of either is!!). Claimed by me
7. ZetaBnd_aux2 begins the analysis inside the critical strip; just bounds an individual term in the Dirichlet series. (Should be very straightforward.) Done by @Paul Nelson
8. ZetaUpperBnd uses the formula in 6. and bound in 7. to give an upper bound for $\zeta(\sigma+it)$ for $1-A/\log t \le \sigma$. Done by @Vláďa Sedláček
9. ZetaDerivUpperBnd Differentiating 8. term by term gives a bound for $\zeta'$. Claimed by me and @Vláďa Sedláček

[Breaking here because of zulip length issues]

[Alex Kontorovich]

[Breaking here because of zulip length issues]

10. ZetaNear1Bnd is an upper bound for the blowup of zeta near 1 (like $1/(s-1)$) for $\Re(s)>1$. (Just adapt riemannZeta_isBigO_near_one_horizontal in @Michael Stoll's EulerProducts.PNT file) Done by @Vláďa Sedláček
11. ZetaInvBound1 is a first upper bound for $1/\zeta$ for $\Re(s)>1$, just using the "Hadamard-de la Vallee Poussin" inequality. (Adapt norm_zeta_product_ge_one in @Michael Stoll's EulerProducts.PNT file) Done by @Vláďa Sedláček
12. ZetaInvBound2 combines 11., 10., and 8. (should be very easy) Done by @Vláďa Sedláček
13. Zeta_eq_int_derivZeta is the fundamental theorem of calculus applied to this setting (also very easy). Done by @Vláďa Sedláček
14. Zeta_diff_Bnd combines 13. with 9.; trivially estimating an integral by the max of the integrand times the length. Done by @Vláďa Sedláček
15. ZetaInvBnd This is the first main goal of this section, proving the upper bound $1/|\zeta(\sigma+it)| \ll \log^7|t|$ for $1-A/\log^9|t| < \sigma <1$. Claimed by me and @Vláďa Sedláček
16. LogDerivZetaBnd And this is the main corollary of 15, used together with 9. Done by @Vláďa Sedláček

With LogDerivZetaBnd in place, we're really very very close to a strong (well, "medium") PNT. I'll be writing up these last steps over the next few days.

On the Fourier/Tauberian side, here are the next goals from Terry:
17. Fourier identity in the Schwartz class This is the first somewhat tricky step in the Fourier argument to formalize: 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. Done by @Vincent Beffara
18. Bijectivity of the Fourier transform Now that the Fourier inversion formula is Mathlib, this is just a matter of showing that the Fourier transform (and its inverse) preserve the Schwartz class. Possibly some of the tools used to establish Decay bounds could be relevant here.
19. Smoothed Wiener-Ikehara The first major milestone towards the Wiener-Ikehara lemma! It should follow readily from Fourier identity in the Schwartz class and Bijectivity of the Fourier transform and some basic algebraic manipulation. Done by @Vincent Beffara
20. Limiting corollary Immediate from Limiting Fourier Identity and the Riemann-Lebesgue lemma Done by @Vincent Beffara

[Michael Stoll]

10. is basically the first have in riemannZeta_isBigO_near_one_horizontal in EulerProducts.PNT .

[Alex Kontorovich]

Great thanks! (Yes, they're meant to be "easy", from what is already done...)

[Michael Stoll]

I see you want it along the real axis and coming from the right. This is riemannZeta_isBigO_near_one_horizontal on the nose, except for a shift σ = 1 + x.

[Michael Stoll]

Note that isBigO_mul_iff_isBigO_div and isBigO_comp_ofReal_nhds_ne are defined locally (the first one in EulerProducts.Auxiliary).

[Michael Stoll]

...and 11 is norm_zeta_product_ge_one in my PNT file (modulo moving terms around). (This is actually mentioned in the blueprint.)

[Michael Stoll]

Theorem 10 is LSeries_vonMangoldt_eq.

[Alex Kontorovich]

Yes, many of these are just assembling in one place the various identities needed...

[Gareth Ma]

Are you working on (1) already?

[Arend Mellendijk]

Regarding partial summation, wouldn't it be better to express $\sum_{a < n \le b} f(n)$ as ∑ n in Finset.Ioc ⌊a⌋ ⌊b⌋, f n rather than ∑ n in Finset.Icc (⌊a⌋ + 1) ⌊b⌋, f n. I think it would make identities like $\sum_{a < n \le b} f(n) + \sum_{b < n \le c} f(n) = \sum_{a < n \le c} f(n)$ easier to prove.

[Sébastien Gouëzel]

The convention in mathlib is rather to use sums $\sum_{a \le n < b} ...$, because over the naturals you can express any sum on an interval like that, while sums $\sum_{a < n \le b}$ can never contain $0$.

[Yaël Dillies]

Sébastien, this is more of an historical artefact that will disappear as soon as I have time

[Yaël Dillies]

Historically, there was only Finset.Ico, then at some point 2 years ago I added Icc, Ioc, Ioo, but didn't have the time to appropriately expand the big operators API. But I will do it soon, at the latest this summer

[Sébastien Gouëzel]

It's not a historical artifact, it's mathematically better to do it this way -- I mean, when you want to sum n terms, most of the time the best way to write it is as a sum from 0 to n-1. So I am strongly in favor that it remains the canonical way to write sums in mathlib, although having more API for the other types of intervals is definitely welcome.

[Yaël Dillies]

Your consideration only applies to intervals starting at zero. I have many summation proofs that are weird because they have shoehorned into the Ico framework.

[Arend Mellendijk]

Sébastien Gouëzel said:

The convention in mathlib is rather to use sums $\sum_{a \le n < b} ...$, because over the naturals you can express any sum on an interval like that, while sums $\sum_{a < n \le b}$ can never contain $0$.

Do note these sums are over Int, so considerations about 0 don't apply directly, though of course the Ico api might be more developed because of it.

[Alex Kontorovich]

Gareth Ma said:

Are you working on (1) already?

Kind of, but not directly. I've been thinking about what's really going on here. It's so obvious to humans, that I find it difficult to state formally. You know something is true on all intervals between two consecutive integers, and can easily prove that it's additive on adjacent intervals, and then want to conclude that it's true on any interval. It's some kind of "induction on intervals". So I've been thinking a bit about what the right API is so that (1) follows easily from sum_eq_int_deriv_aux2 (which itself isn't completely finished either...)

[Alex Kontorovich]

I'll claim (1) for now, to try out @Sébastien Gouëzel's suggestion to change to Ico. Though as @Arend Mellendijk points out, I'm working here over Int, not Nat, so maybe it's not essential to make the change... (I'd have to slightly change the mathematics to get it to work...)

[Alex Kontorovich]

I think this is the statement I have in mind. Kinda weird... but also cool?...

import Mathlib

lemma intervalInduction {P : ℝ → ℝ → Prop}
    (h₁ : ∀ (a b : ℝ) (k : ℤ) (k_le_a : k ≤ a) (a_lt_b : a < b) (b_le_k1 : b ≤ k + 1), P a b)
    (h₂ : ∀ (a b : ℝ) (k : ℤ) (k_le_a : k ≤ a) (a_lt_k1 : a < k + 1) (k1_lt_b : k + 1 < b)
      (b_le_k2 : b ≤ k + 2), P a b)
    {a b : ℝ} (a_lt_b : a < b) : P a b := by sorry

You induct on the number of integers between $a$ and $b$. I'll try to see if I can prove it myself (no hints please, for now!...)

[Yaël Dillies]

@Alex J. Best and I have this induction principle in LeanCamCombi

[Vincent Beffara]

This sounds like saying "if the property holds for every interval containing no integer, and also for each interval containing at least one integer, then it holds for every interval" Read too fast sorry...

[Vincent Beffara]

So the induction scheme is this?

lemma intervalInduction {P : ℝ → ℝ → Prop}
    (h₁ : ∀ (a b : ℝ) (a_lt_b : a < b), ∀ (k : ℤ), ↑k ∈ Set.Icc (b - 1) a → P a b)
    (h₂ : ∀ (a b : ℝ) (a_lt_b : a < b), ∀ (k : ℤ),
      ↑k ∈ Set.Icc (b - 2) a ∩ Set.Ioo (a - 1) (b - 1) → P a b)
    {a b : ℝ} (a_lt_b : a < b) : P a b := by sorry

[Vincent Beffara]

IOW, if P a b holds whenever Set.Icc (b - 1) a intersects Z, and whenever Set.Icc (b - 2) a ∩ Set.Ioo (a - 1) (b - 1) intersects Z, then it holds all the time?

[Arend Mellendijk]

I don't think the statement is quite right. Surely there is no way to conclude P 0 10 without assuming transitivity of some form? I think we'd want something more like this.

lemma interval_induction (P : ℝ → ℝ → Prop)
    (base : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (step : ∀ a b c : ℝ, a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a b : ℝ) (hab : a ≤ b) : P a b := sorry

(and I have a proof, but Alex Kontorovich asked for no hints :grinning_face_with_smiling_eyes: )

[Vincent Beffara]

That feels weird because if P says "a is not much smaller than b` then both h1 and h2 are vacuously true

[Alex Kontorovich]

Yaël Dillies said:

Alex J. Best and I have this induction principle in LeanCamCombi

Wild! Can you point me to it please?

[Alex Kontorovich]

Arend Mellendijk said:

I don't think the statement is quite right. Surely there is no way to conclude P 0 10 without assuming transitivity of some form? I think we'd want something more like this.

lemma interval_induction (P : ℝ → ℝ → Prop)
    (base : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (step : ∀ a b c : ℝ, a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a b : ℝ) (hab : a ≤ b) : P a b := sorry

(and I have a proof, but Alex Kontorovich asked for no hints :grinning_face_with_smiling_eyes: )

In my application, I don't think I can verify step; I can only do it if b is an integer. (Yeah, you can send the proof; I've been in meetings since my post ... I was hoping I could ignore the calls and play with the proof, but then unfortunately I actually had to pay attention and participate...)

[Arend Mellendijk]

The inductive step here doesn't quite go through if you change b to be an integer, but it shouldn't be too difficult to adapt the proof.

variable {α : Type*} [LinearOrderedRing α] [FloorRing α] in
theorem Int.le_floor_add_one (a : α) : a ≤ ⌊a⌋ + 1 := by
  calc a ≤ ⌈a⌉ := by exact le_ceil a
    _ ≤ ⌊a⌋ + 1 := by norm_cast; exact ceil_le_floor_add_one a

variable {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] in
theorem Nat.le_floor_add_one (a : α) : a ≤ ⌊a⌋₊ + 1 := by
  calc a ≤ ⌈a⌉₊ := by exact le_ceil a
    _ ≤ ⌊a⌋₊ + 1 := by norm_cast; exact ceil_le_floor_add_one a

lemma interval_induction_aux (n : ℕ) :  ∀ (P : ℝ → ℝ → Prop)
    (_ : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (_ : ∀ a b c : ℝ, a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a b : ℝ) (_ : a ≤ b) (_ : n ≤ b-a) (_ : b-a ≤ n+1),
    P a b := by
  induction n using Nat.case_strong_induction_on with
  | hz =>
    intro P base step a b hab _ hn'
    norm_num at hn'
    have : Int.floor b ≤ b := Int.floor_le b
    by_cases hab' : a ≤ Int.floor b
    · apply step a (Int.floor b) b hab' (Int.floor_le b)
      · apply base _ _ (Int.floor b - 1)
        · simp only [Int.cast_sub, Int.cast_one, tsub_le_iff_right]
          linarith
        · exact hab'
        · simp
      · apply base _ _ (Int.floor b) <;> linarith
    · rw [not_le] at hab'
      apply base _ _ (Int.floor b) (by linarith) hab (Int.le_floor_add_one _)
  | hi n ih =>
    intro P base step a b _ hn hn'
    norm_num at hn hn'
    apply step a (a+1) b
    · linarith
    · linarith
    · apply ih 0 (Nat.zero_le n) P base step <;> norm_num
    · apply ih n le_rfl P base step <;> linarith

lemma interval_induction (P : ℝ → ℝ → Prop)
    (base : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (step : ∀ a b c : ℝ, a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a b : ℝ) (hab : a ≤ b) : P a b := by
  apply interval_induction_aux (Nat.floor (b-a)) P base step a b hab (Nat.floor_le (by linarith))
    (Nat.le_floor_add_one _)

[Arend Mellendijk]

Here's the integer version:

code

variable {α : Type*} [LinearOrderedRing α] [FloorRing α] in
theorem Int.le_floor_add_one (a : α) : a ≤ ⌊a⌋ + 1 := by
  calc a ≤ ⌈a⌉ := by exact le_ceil a
    _ ≤ ⌊a⌋ + 1 := by norm_cast; exact ceil_le_floor_add_one a

variable {α : Type*} [LinearOrderedSemiring α] [FloorSemiring α] in
theorem Nat.le_floor_add_one (a : α) : a ≤ ⌊a⌋₊ + 1 := by
  calc a ≤ ⌈a⌉₊ := by exact le_ceil a
    _ ≤ ⌊a⌋₊ + 1 := by norm_cast; exact ceil_le_floor_add_one a

lemma interval_induction_aux_int (n : ℕ) :  ∀ (P : ℝ → ℝ → Prop)
    (_ : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (_ : ∀ a : ℝ, ∀ b c : ℤ, a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a : ℝ) (b : ℤ) (_ : a ≤ b) (_ : n ≤ b-a) (_ : b-a ≤ n+1),
    P a b := by
  induction n using Nat.case_strong_induction_on with
  | hz =>
    intro P base _ a b hab _ hn'
    norm_num at hn'
    apply base a b (b-1) (by push_cast; linarith) hab (by norm_num)
  | hi n ih =>
    intro P base step a b _ hn hn'
    norm_num at hn hn'
    rw [show (n + 1 + 1 : ℝ) = n + 2 by ring] at hn'
    apply step a (b-1) b
    · push_cast; linarith
    · linarith
    · apply ih n le_rfl P base step <;> push_cast <;> linarith
    · apply ih 0 (Nat.zero_le n) P base step <;> norm_num

lemma interval_induction' (P : ℝ → ℝ → Prop)
    (base : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (step : ∀ (a : ℝ) (b c : ℤ), a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a : ℝ) (b : ℤ) (hab : a ≤ b) : P a b := by
  apply interval_induction_aux_int (Nat.floor (b-a)) P base step a b hab (Nat.floor_le (by linarith))
    (Nat.le_floor_add_one _)

lemma interval_induction (P : ℝ → ℝ → Prop)
    (base : ∀ a b : ℝ, ∀ k : ℤ, k ≤ a → a ≤ b → b ≤ k+1 → P a b)
    (step : ∀ (a : ℝ) (b : ℤ) (c : ℝ), a ≤ b → b ≤ c → P a b → P b c → P a c)
    (a b : ℝ) (hab : a ≤ b) : P a b := by
  by_cases hab' : a ≤ Int.floor b
  · apply step a (Int.floor b) b hab' (Int.floor_le b)
    · apply interval_induction' P base (fun a b c ↦ by simpa using step a b c) _ _ hab'
    · apply base _ _ (Int.floor b) <;> norm_num
      · exact Int.floor_le b
      · exact Int.le_floor_add_one b
  · rw [not_le] at hab'
    apply base _ _ (Int.floor b) hab'.le hab (Int.le_floor_add_one b)

[Paul Nelson]

I can try 3. ZetaSum_aux1a

[Alex Kontorovich]

Awesome, thanks! Let me know if you want to do it yourself, or if you want to hop on zoom and keep playing...

[Paul Nelson]

tonight I reduced ZetaSum_aux1a to a couple integrability checks: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/commit/79064cfb0b106fde554b6f28d821eb3fa1f11162

[Alex Kontorovich]

Great! PR what you have, and others can try to help...

[Paul Nelson]

did so just now. reduced it further to a measurability check, see https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/commit/c54dd71ebedad1ede2bcfb36b94295c289ab74dc or below:

theorem ZetaSum_aux1a_aux5c {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) :
  let g : ℝ → ℝ := fun u ↦ |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1);
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι a b)) := by sorry

I didn't spot basic API for working with ratios like this

[llllvvuu]

For measurability things I try to make it work with fun_prop, tracing and apply?ing at points where it gets stuck. The hope is to be able to discover new places where a @[fun_prop] tag could be added upstream

(Usually get blocked by side conditions though and then I end up spamming apply then cleaning up)

[llllvvuu]

Here's a proof (tactics didn't seem to do too well here):

import Mathlib.MeasureTheory.Function.Floor

-- TODO: why do we need to bump this?
instance : MeasurableDiv₂ ℝ := by
  haveI (G : Type) [DivInvMonoid G] [MeasurableSpace G] [MeasurableInv G] [MeasurableMul₂ G] :
    MeasurableDiv₂ G := inferInstance
  exact this ℝ

...

  apply Measurable.aestronglyMeasurable
  apply Measurable.div
  · apply (_root_.continuous_abs).measurable.comp
    · apply Measurable.sub
      · apply Measurable.add
        · apply Measurable.comp
          · exact fun _ _ ↦ trivial
          · exact Int.measurable_floor
        · exact measurable_const
      · exact measurable_id
  · exact measurable_id.pow_const _

[Paul Nelson]

OK, thanks! do you want to append this to the PR, or should I just copy/paste it in?

[llllvvuu]

Feel free to copy paste at your own leisure!

[Paul Nelson]

thanks. I did so and tried to PR just now, but the PR attempt failed the following check:

error: stdout:
./././PrimeNumberTheoremAnd/SecondProofPNT.lean:1:0: error: import PrimeNumberTheoremAnd.ZetaBounds failed, environment already contains 'instMeasurableDiv₂RealMeasurableSpaceToDivInstLinearOrderedFieldReal' from PrimeNumberTheoremAnd.PerronFormula

This is related to the instance from your snippet.

[llllvvuu]

Interesting :thinking: maybe see if removing that part works?

Otherwise I'd be happy to update the PR later when I'm back at my computer

[Paul Nelson]

it doesn't. for some reason #check (inferInstance : MeasurableDiv₂ ℝ) works in SecondProofPNT.lean, but not in ZetaBounds.lean. I'll poke around w/ the instances some

[Paul Nelson]

ah, I see now. the point was that the same hack instance : MeasurableDiv₂ ℝ ... had already been used in PerronFormula.lean, and was getting included twice in SecondProofPNT.lean. so maybe that instance should go in some "common" file? is there a good convention?

anyway, tried PR'ing again (after replacing that instance w/ an import of PerronFormula) and checks passed, so I guess we can cross off item (3)

[Paul Nelson]

I could try 19 next. seems like one step is to check that (smooth, compact support) implies Schwartz, which I didn't spot anywhere. I guess it would be formulated something like this?

lemma schwartz_of_smooth_compact_support (f : ℝ → ℂ) (hsmooth: ∀ n, ContDiff ℝ n f) (hsupp: HasCompactSupport f)
    : ∃ g : SchwartzMap ℝ ℂ, g = f := by
  sorry

[Alex Kontorovich]

Paul Nelson said:

I could try 19 next. seems like one step is to check that (smooth, compact support) implies Schwartz, which I didn't spot anywhere. I guess it would be formulated something like this?

lemma schwartz_of_smooth_compact_support (f : ℝ → ℂ) (hsmooth: ∀ n, ContDiff ℝ n f) (hsupp: HasCompactSupport f)
    : ∃ g : SchwartzMap ℝ ℂ, g = f := by
  sorry

19 is yours! I think hsmooth can be spelled: ContDiff ℝ ⊤ f. I indeed didn't see this theorem in the library, so would be great to add it (and shouldn't be too hard...?). Thanks Paul!!

[llllvvuu]

Could also be a def that returns SchwartzMap \R \C; I'm not sure what the "best practice" is though

[Alex Kontorovich]

Good point! Yes, that might be the preferred practice, not to prove the existence, but to exhibit the property...

[Vincent Beffara]

def toSchwartz (f : ℝ → ℂ) (h1 : ContDiff ℝ ⊤ f) (h2 : HasCompactSupport f) : 𝓢(ℝ, ℂ) where
  toFun := f
  smooth' := h1
  decay' k n := by
    have l1 : Continuous (fun x => ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by
      have : ContDiff ℝ ⊤ (iteratedFDeriv ℝ n f) := h1.iteratedFDeriv_right le_top
      exact Continuous.mul (by continuity) this.continuous.norm
    have l2 : HasCompactSupport (fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := (h2.iteratedFDeriv _).norm.mul_left
    simpa using l1.bounded_above_of_compact_support l2

[Vincent Beffara]

In fact I just started as well on wiener_ikehara_smooth which is why I needed this lemma ...

[Paul Nelson]

ah cool

[Paul Nelson]

you can have it if you'd like, I'll just paste here the small amount I did tonight:

lemma wiener_ikehara_smooth_aux1 (n : ℕ∞) :
    ContDiff ℝ n ((λ x => x) : ℝ → ℂ) := by
  sorry

lemma wiener_ikehara_smooth {Ψ: ℝ → ℂ} (hsmooth: ∀ n, ContDiff ℝ n Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi (0:ℝ)) :
    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n/x))/x - A * ∫ y in Set.Ioi 0, Ψ y ∂ volume)
    atTop (nhds 0) := by
  set ψ₀ : ℝ → ℂ := λ x => (cexp x) * Ψ (exp x)
  have hsmooth₀ : ∀ n, ContDiff ℝ n ψ₀ := by
    intro n
    apply ContDiff.mul
    · apply ContDiff.cexp
      exact wiener_ikehara_smooth_aux1 n
    · apply ContDiff.comp
      · exact hsmooth n
      · exact Real.contDiff_exp
  set times_two_pi : ℝ → ℝ := λ x => 2 * π * x
  set ψ₁ : ℝ → ℂ := λ x => (ψ₀ ∘ times_two_pi) x
  have hsmooth₁ : ∀ n, ContDiff ℝ n ψ₁ := by
    intro n
    apply ContDiff.comp
    · exact hsmooth₀ n
    · apply ContDiff.mul
      · exact contDiff_const
      · exact contDiff_id
  have hsupp₁ : HasCompactSupport ψ₁ := by
    sorry
  have : ∃ ψ₂ : SchwartzMap ℝ ℂ, ψ₂ = ψ₁ := by
    exact schwartz_of_smooth_compact_support hsmooth₁ hsupp₁
  obtain ⟨ψ₂, hψ₂⟩ := this
  have := fourier_surjection_on_schwartz ψ₂
  obtain ⟨ψ, hψ⟩ := this
  have hRHS : (∫ y in Set.Ioi 0, Ψ y ∂ volume)
       = ∫ (u : ℝ), 𝓕 ψ (u / (2 * π)) := by sorry -- change of variable
  have : Ψ = fun u => ψ₁ (Real.log u) / u := by sorry
  rw [this]
  simp only [ofReal_div, ofReal_nat_cast]
  rw [← hψ₂]
  rw [← hψ]
  have hLHS : ((∑' n, f n * Ψ (n/x))/x)
       = ∑' n, f n / n * 𝓕 ψ (1 / (2 * π) * log (n / x)) := by sorry

  sorry

(not edited or necessarily correct or anything)

[Vincent Beffara]

Here is where I am:

@[simp] lemma toSchwartz_apply (f : ℝ → ℂ) {h1 h2 x} : SchwartzMap.mk f h1 h2 x = f x := rfl

@[simp] lemma why (x : ℝ) : 2 * π * x / (2 * π) = x := by field_simp ; ring

lemma wiener_ikehara_smooth (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f)
    (hG: ContinuousOn G {s | 1 ≤ s.re}) (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
    {Ψ: ℝ → ℂ} (hsmooth: ContDiff ℝ ⊤ Ψ) (hsupp: HasCompactSupport Ψ)
    (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x - A * ∫ y in Set.Ioi 0, Ψ y ∂ volume) atTop (nhds 0) := by

  let h (x : ℝ) : ℂ := rexp (2 * π * x) * Ψ (exp (2 * π * x))
  have h1 : ContDiff ℝ ⊤ h := sorry
  have h2 : HasCompactSupport h := sorry
  obtain ⟨g, hg⟩ := fourier_surjection_on_schwartz (toSchwartz h h1 h2)

  have l1 {y} (hy : 0 < y) : y * Ψ y = 𝓕 g (1 / (2 * π) * Real.log y) := by
    field_simp [hg, toSchwartz, h] ; norm_cast ; field_simp ; norm_cast
    rw [Real.exp_log hy]

  have key := @limiting_cor_schwartz f A G g hf hcheby hG hG'

  have l2 : ∀ᶠ x in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * Real.log (↑n / x)) =
      ∑' (n : ℕ), f n * Ψ (↑n / x) / x := by
    filter_upwards [eventually_gt_atTop 0] with x hx
    congr ; ext n
    by_cases hn : n = 0 ; simp [hn]
    rw [← l1 (by positivity)]
    have : (n : ℂ) ≠ 0 := by simpa using hn
    have : (x : ℂ) ≠ 0 := by simpa using hx.ne.symm
    field_simp ; ring

  have l3 : ∀ᶠ x in atTop, ↑A * ∫ (u : ℝ) in Ici (-Real.log x), 𝓕 (⇑g) (u / (2 * π)) =
      ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y := by
    filter_upwards [eventually_gt_atTop 0] with x hx
    congr 1

    sorry

[Paul Nelson]

cool. so I guess I worked out something like your "h1"

[Vincent Beffara]

Yes exactly, I'm going to steal it :-) The last sorry is (well, should be) a simple change of variable. And h2 should not be too hard, but I'm slightly afraid of it...

[Paul Nelson]

for h2, I figured one would have to show that a compact subset of the positive reals that did not contain 0 is contained in some interval [a,b] with positive endpoints, and then pull this back via the logarithm. but I wondered if it might be slightly easier to tweak the formulation to say explicitly "this function is supported on [a,b] for some 0 < a < b" rather than to formulate things topologically (assuming that such a tweak would not affect usage elsewhere)

[Vincent Beffara]

I wanted to use docs#hasCompactSupport_iff_eventuallyEq and to say that exp x as x goes to eventually exits the support (but this still needs the fact that the support is contained in such an [a, b])

[Paul Nelson]

very well. GL HF. I'll relinquish 19 and try 7 tomorrow night

[llllvvuu]

In one dimension we have docs#cocompact_eq_atBot_atTop for R and docs#cocompact_eq_atTop for R+

Maybe combined with docs#Filter.EventuallyEq.comp_tendsto could do the trick

[llllvvuu]

(deleted)

[llllvvuu]

Maybe this is an easier goal:

lemma Filter.EventuallyEq.sup_filter {α β : Type*} {f g : α → β} {l l' : Filter α} :
    f =ᶠ[l ⊔ l'] g ↔ f =ᶠ[l] g ∧ f =ᶠ[l'] g := by
  simp_rw [EventuallyEq, Filter.eventually_sup]

...

  have h2 : HasCompactSupport h := by
    show HasCompactSupport ((fun x ↦ ((rexp (2 * π * x)) : ℂ)) • (fun x ↦ Ψ (rexp (2 * π * x))))
    apply HasCompactSupport.smul_left
    rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact,
      cocompact_eq_atBot_atTop, EventuallyEq.sup_filter] at hsupp ⊢
    constructor
    · sorry -- ⊢ (fun x ↦ Ψ (rexp (2 * π * x))) =ᶠ[atBot] 0
    · apply (show Ψ =ᶠ[atTop] 0 from hsupp.2).comp_tendsto
      sorry -- ⊢ Tendsto (fun x ↦ rexp (2 * π * x)) atTop atTop

[Vincent Beffara]

theorem comp_exp_support {Ψ : ℝ → ℂ} (hsupp : HasCompactSupport Ψ) (hplus : closure (Function.support Ψ) ⊆ Ioi 0) :
    HasCompactSupport (Ψ ∘ rexp) := by

  simp only [hasCompactSupport_iff_eventuallyEq, EventuallyEq, coclosedCompact_eq_cocompact,
    cocompact_eq_atBot_atTop, eventually_sup, Pi.zero_apply] ; constructor
  · simp [← disjoint_compl_right_iff_subset] at hplus
    obtain ⟨δ, hδ, hdisj⟩ := hplus.exists_thickenings hsupp isClosed_Iic
    have l1 : Metric.thickening δ (Iic (0 : ℝ)) ∈ 𝓝 0 := by
      refine mem_of_superset (Metric.ball_mem_nhds 0 hδ) ?_
      exact Metric.ball_subset_thickening (mem_Iic.mpr le_rfl) δ
    have l2 : ∀ᶠ x in atBot, rexp x ∈ Metric.thickening δ (Iic 0) := Real.tendsto_exp_atBot l1
    filter_upwards [l2] with x hx
    have := hdisj.subset_compl_left hx
    have := compl_subset_compl.mpr (Metric.self_subset_thickening hδ _) this
    have := compl_subset_compl.mpr subset_closure this
    simpa using this
  · simp [hasCompactSupport_iff_eventuallyEq] at hsupp
    exact Real.tendsto_exp_atTop hsupp.2

[Vláďa Sedláček]

I just finished 16. to get a taste of this section and I can do 12.-15. in the near future.

[Vincent Beffara]

19. is done, modulo surjectivity of the Fourier transform on the Schwartz class.

[Vincent Beffara]

I added the surjectivity as an axiom to make sure that there were no other sorries missing:

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

[Vincent Beffara]

I also removed the assumption that f 0 = 0 from most of Wiener.lean and switched all statements from ArithmeticFunction to N \to C to make them more flexible.

[Vincent Beffara]

I am looking at WienerIkeharaInterval and it is going to be a bit annoying, because everything switches to real-valued sequences to use order. But the previous results are for complex-values sequences so it is not easy to use them. I think I am planning to replace everywhere ℂ with {𝕜 : Type*} [IsROrC 𝕜] so that we don't have to prove two versions of each lemma ... except that term wants complex numbers.

[Alex Kontorovich]

Yes, we had a similar problem with MellinTransform, so had to make the [IsROrC] move, so I'm not surprised... Sorry! :(

[Vincent Beffara]

I cannot touch term which is in Mathlib, so the move to IsROrC is a bit tricky to do :-( I am trying this instead

local instance {E : Type*} : Coe (E → ℝ) (E → ℂ) := ⟨fun f n => f n⟩

and hoping for the best.

[Michael Stoll]

Note that IsRorC is nowadays called docs#RCLike .

[Michael Stoll]

There might also be the option of using the ordering on the complex numbers (docs#Complex.partialOrder), available via open scoped ComplexOrder. But likely using RCLike is nicer.

[llllvvuu]

I cannot touch term which is in Mathlib,

the location might matter less than whether the change makes sense

[Vincent Beffara]

the location means that changing the def involves either forking Mathlib to make the change and base PNT+ on that, or PRing the change and waiting for review and such

[Vincent Beffara]

Michael Stoll said:

Note that IsRorC is nowadays called docs#RCLike .

I didn't know! When did this occur?

[Michael Stoll]

When #10819 was merged last week.

[Vincent Beffara]

OK so this is not too bad:

lemma wiener_ikehara_smooth' (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f)
    (hG: ContinuousOn G {s | 1 ≤ s.re}) (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
    (hsmooth: ContDiff ℝ ⊤ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x) atTop (nhds (A * ∫ y in Set.Ioi 0, Ψ y)) :=
  tendsto_sub_nhds_zero_iff.mp <| wiener_ikehara_smooth hf hcheby hG hG' hsmooth hsupp hplus

local instance {E : Type*} : Coe (E → ℝ) (E → ℂ) := ⟨fun f n => f n⟩

@[norm_cast]
theorem set_integral_ofReal {f : ℝ → ℝ} {s : Set ℝ} : ∫ x in s, (f x : ℂ) = ∫ x in s, f x :=
  integral_ofReal

lemma wiener_ikehara_smooth_real {f : ℕ → ℝ} {Ψ : ℝ → ℝ} (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')) (hcheby : cheby f)
    (hG: ContinuousOn G {s | 1 ≤ s.re}) (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})
    (hsmooth: ContDiff ℝ ⊤ Ψ) (hsupp: HasCompactSupport Ψ) (hplus: closure (Function.support Ψ) ⊆ Set.Ioi 0) :
    Tendsto (fun x : ℝ ↦ (∑' n, f n * Ψ (n / x)) / x) atTop (nhds (A * ∫ y in Set.Ioi 0, Ψ y)) := by

  let Ψ' := ofReal' ∘ Ψ
  have l1 : ContDiff ℝ ⊤ Ψ' := contDiff_ofReal.comp hsmooth
  have l2 : HasCompactSupport Ψ' := hsupp.comp_left rfl
  have l3 : closure (Function.support Ψ') ⊆ Ioi 0 := by rwa [Function.support_comp_eq] ; simp
  have key := (continuous_re.tendsto _).comp (@wiener_ikehara_smooth' A Ψ G f hf hcheby hG hG' l1 l2 l3)
  simp at key ; norm_cast at key

[Vincent Beffara]

I've made good progress on WienerIkeharaInterval, a few sorries left but nothing major I believe, the current code is at https://github.com/vbeffara/PNT/blob/d77dfe42843896bf651bfbfc9c76681ae218d655/PrimeNumberTheoremAnd/Wiener.lean#L1775

In retrospect it would have been much nicer in some respects to work in ENNReal, a wonderful place where liminf is always below limsup ...

[Alex Kontorovich]

Do you think it's worth a refactor? As we near PNT (in both weak and medium form), I'm starting to think about what it'll take to port this all to mathlib. It'll be a big job!... (Of course we'll need to split into lots of little PRs) Maybe we'll keep up the momentum through Dirichlet, and then pause to port before embarking on Chebotarev, something like that?... TBD...

[Alex Kontorovich]

FYI 2. ZetaSum_aux1 is now done, modulo Real.differentiableAt_cpow_const_of_ne. PRing now.

[Terence Tao]

Vincent Beffara said:

I've made good progress on WienerIkeharaInterval, a few sorries left but nothing major I believe, the current code is at https://github.com/vbeffara/PNT/blob/d77dfe42843896bf651bfbfc9c76681ae218d655/PrimeNumberTheoremAnd/Wiener.lean#L1775

In retrospect it would have been much nicer in some respects to work in ENNReal, a wonderful place where liminf is always below limsup ...

In the event that we choose this route, I extended the blueprint at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/147 to show how to remove the Chebyshev hypothesis from the Wiener-Ikehara theorem.

[Alex Kontorovich]

Great thanks!

[Vincent Beffara]

WienerIkeharaInterval is done at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/148

[Vincent Beffara]

(But I did changes that break MellinCalculus.lean, let me fix them real quick.)

[Vincent Beffara]

Done!

[Vincent Beffara]

Followint the whole Icc vs Ico discussion I rewrote the interval version of Wiener-Ikehara using Ico everywhere, and then wrote a Finset version:

lemma WienerIkeharaInterval_discrete' {f : ℕ → ℝ} (hpos : 0 ≤ f) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))
    (hcheby : cheby f) (hG: ContinuousOn G {s | 1 ≤ s.re})
    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re}) (ha : 0 < a) (hb : a < b) :
    Tendsto (fun N : ℕ ↦ (∑ n in Finset.Ico ⌈a * N⌉₊ ⌈b * N⌉₊, f n) / N) atTop (nhds (A * (b - a)))

from which WienerIkeharaTheorem' should readily follow. And indeed the API around Ico is much nicer to use, no need to juggle with floor and ceil and so on.

[Paul Nelson]

ZetaBnd_aux2 (item 7): https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/152