OAI/NumberTheory/TwoPoint/Bounds/PrimeDefectBias.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Persistent ordinary two-point bias forces finite reciprocal prime-modulus defect for both factors. This is an elementary consequence of the p² CRT majorant, with no additional mean-value input.

  1. lemma OAI.TwoPointCorrelations.shifted_modulus_sum_le line 15
  2. lemma OAI.TwoPointCorrelations.normalized_correlation_le_first_modulus line 33
  3. lemma OAI.TwoPointCorrelations.normalized_correlation_le_second_modulus line 45
  4. theorem OAI.TwoPointCorrelations.correlation_zero_of_first_modulus_mean_zero line 58
  5. theorem OAI.TwoPointCorrelations.correlation_zero_of_second_modulus_mean_zero line 67
  6. theorem OAI.TwoPointCorrelations.persistent_correlation_prime_defects line 79
  7. theorem OAI.TwoPointCorrelations.persistent_correlation_one_values line 94