mobius lemma 2

Stream: PrimeNumberTheorem+

[Steven Rossi]

I'm working on the final lemma of mobius, and having problems with us using Finset.range for some definitions, while using Finset.Ioc for others. This adds 0 in the index of some summations and then the sqrt in M has a divide by 0. How do we want to deal with this? Or maybe I'm misunderstanding some definition

[Yongxi Lin (Aaron)]

It shouldn't be a problem right? Dividing by zero is equal to zero and square root of zero is zero, and I believe the definition of M also forces M 0 to be zero.

[Steven Rossi]

Ah ok is that the convention in mathlib? Sounds good

[Yongxi Lin (Aaron)]

Yes you can find these conventions in Mathlib: div_zero, Real.sqrt_zero. Also M x = ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ..., so when x = 0, Finset.Ioc 0 ⌊x⌋₊ is empty, and we have Finset.sum_of_isEmpty

[Terence Tao]

It may not be possible to align all the notations to be consistent about this, but if you find that changing the range of summation in a theorem to either add or remove a zero simplifies the proof, without significantly impacting how this result might be used downstream, you are welcome to change the theorem statement to streamline the proof a little bit.

[Steven Rossi]

Seems like the proper way to do it in mathlib would define M as an ArithmeticFunction but :man_shrugging:

[Terence Tao]

The function $M(x)$ most naturally takes real values, as opposed to ArithmeticFunction which takes natural number values. It's true that one has $M(x) = M(⌊x⌋₊)$ for all $x$ but given that we are frequently using real number operations such as working with $M √(x/k)$ I'm not sure it would be all that advantageous to switch over to natural number domains.

[Steven Rossi]

Should the mobius_lemma_2 have

  2 * x *
    ∑ k ∈ Finset.Ico (K + 1) (⌊x⌋₊ + 1),
      ∫ t in Real.sqrt (x / (k + 0.5))..Real.sqrt (x / (k - 0.5)),
        ((M t - M (Real.sqrt (x / k))) : ℝ) / t ^ 3

part of its definition? This varies from the blueprint

[Terence Tao]

Ah, I tracked down what happened. The LaTeX source for this blueprint contained some additional formulas that had been commented out; but I was relying on Github Copilot's autocomplete function to accelerate my conversion of this LaTeX to Lean form, and the autocomplete "helpfully" also formalized the commented formula without realizing that it was not to be included, and I did not review it carefully enough to catch it. Part of the inherent risk in relying on AI tools, but I think the tradeoff of increased speed at the cost of (fixable) inaccuracy is manageable, especially since we often have a digital "paper trail" to identify where the errors came from. Anyway, as you have claimed this task, feel free to change the lemma statement to align with the blueprint (and, hopefully, align also with what can actually be proven).