OAI/NumberTheory/TwoPoint/Bounds/ActualPaddingWeights.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The graph's literal padding weight and vertex normalization. The normalization is the square root of 5^omega_Q(n) and depends only on the padding-prime residues, including at the integer zero.

  1. def OAI.TwoPointCorrelations.actualPaddingDegree line 15
  2. def OAI.TwoPointCorrelations.actualPaddingWeight line 18
  3. def OAI.TwoPointCorrelations.actualPaddingVertex line 21
  4. def OAI.TwoPointCorrelations.actualPaddingCoefficient line 24
  5. lemma OAI.TwoPointCorrelations.actualPaddingCoefficient_nonneg line 27
  6. lemma OAI.TwoPointCorrelations.actualPaddingWeight_one_le line 31
  7. lemma OAI.TwoPointCorrelations.actualPaddingVertex_one_le line 34
  8. lemma OAI.TwoPointCorrelations.actualPaddingVertex_pos line 38
  9. lemma OAI.TwoPointCorrelations.actualPaddingVertex_ne_zero line 41
  10. lemma OAI.TwoPointCorrelations.actualPaddingVertex_sq line 44
  11. lemma OAI.TwoPointCorrelations.actualPaddingDegree_residue_congr line 48
  12. lemma OAI.TwoPointCorrelations.actualPaddingWeight_residue_congr line 59
  13. lemma OAI.TwoPointCorrelations.actualPaddingVertex_residue_congr line 65
  14. def OAI.TwoPointCorrelations.actualPaddingDegreeCut line 71
  15. lemma OAI.TwoPointCorrelations.actualPaddingDegreeCut_residue_congr line 74
  16. lemma OAI.TwoPointCorrelations.actualPaddingDegree_eq_available line 80
  17. lemma OAI.TwoPointCorrelations.actualPaddingWeight_eq_tilt line 86
  18. lemma OAI.TwoPointCorrelations.actualPaddingWeight_eq_divisor_sum line 92
  19. def OAI.TwoPointCorrelations.actualPaddingBin line 98
  20. lemma OAI.TwoPointCorrelations.actualPaddingDensity_eq_integerBin line 103

    Source documentation

    With all squarefree padding divisors available, the graph density is exactly the literal normalized bin mass.

    lemma actualPaddingDensity_eq_integerBin (Q : Finset ℕ) (n : ℤ) (η c : ℝ) (j : ℤ) :
    paddingDensity (retainedPrimeDivisors Q) actualPaddingCoefficient
      (actualPaddingBin η c j) (actualPaddingVertex Q) n =
      integerPaddingBinMass Q n η c j := by
…

    Mentions: OAI.TwoPointCorrelations.paddingDensity, OAI.TwoPointCorrelations.retainedPrimeDivisors, OAI.TwoPointCorrelations.actualPaddingCoefficient, OAI.TwoPointCorrelations.actualPaddingBin, OAI.TwoPointCorrelations.actualPaddingVertex, OAI.TwoPointCorrelations.integerPaddingBinMass

  21. lemma OAI.TwoPointCorrelations.actualPaddingDensity_nonneg line 128
  22. lemma OAI.TwoPointCorrelations.actualPaddingDensity_le_one line 139
  23. lemma OAI.TwoPointCorrelations.actualPaddingDensity_le_integerBin line 165
  24. lemma OAI.TwoPointCorrelations.actualPaddingDensity_residue_congr line 178
  25. lemma OAI.TwoPointCorrelations.actualPaddingKeep_residue_congr line 188