OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeRowTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The giant-only prime-to-integer row transfer in Section 7.5

The compensation product stays in the modulus. Only the actual giant prime is averaged with its smooth harmonic prior, so no tuple-factorial loss occurs.

  1. theorem OAI.Ostmann.moving_prime_row_transfer line 16