OAI/NumberTheory/CubicMoment/Estimates/FullPrimeModelOverlap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The factored squarefree model and μ²(ab) differ by a negligible shared-prime sum for the actual independent rough-prime convolution.

  1. theorem OAI.CubicFirstMoment.full_prime_model_overlap_log_saving line 15