OAI/NumberTheory/TwoPoint/Bounds/PaddingDivisorEncoding.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Squarefree padding divisors encode prime selections without multiplicity. This identifies the bin law with the paper's numerical divisor sum.

  1. def OAI.TwoPointCorrelations.paddingAvailablePrimes line 13
  2. lemma OAI.TwoPointCorrelations.paddingAvailablePrimes_subset line 16
  3. lemma OAI.TwoPointCorrelations.mem_paddingAvailablePrimes line 22
  4. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_eq_prod line 33
  5. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_primeFactors line 40
  6. lemma OAI.TwoPointCorrelations.paddingAvailablePrimes_card line 45
  7. lemma OAI.TwoPointCorrelations.padding_supported_iff_primeFactors_subset line 49
  8. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_injective line 63
  9. lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_mem line 73
  10. lemma OAI.TwoPointCorrelations.exists_paddingSelection line 79
  11. def OAI.TwoPointCorrelations.paddingDivisorEquiv line 95
  12. def OAI.TwoPointCorrelations.literalPaddingBinMass line 104

    Source documentation

    rho_j as a sum over actual numerical squarefree divisors.

    noncomputable def literalPaddingBinMass (Q : Finset ℕ) (a : Q → Bool)
    (η c : ℝ) (j : ℤ) : ℝ :=
…
  13. lemma OAI.TwoPointCorrelations.paddingBinMass_eq_literal line 112
  14. lemma OAI.TwoPointCorrelations.paddingTiltNormalizer_eq_divisor_sum line 142
  15. lemma OAI.TwoPointCorrelations.padding_divisor_weight_total line 151