OAI/NumberTheory/TwoPoint/Bounds/PrimeRelations.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Exact prime-variable relations

A monomial has one factor for each distinct label in a squarefree tuple. Its integer coefficient contains the orientation, common shift multiplier, and padding. Numerical coincidences among different labels are allowed.

  1. structure OAI.TwoPointCorrelations.PrimeMonomial line 17
  2. def OAI.TwoPointCorrelations.PrimeMonomial.eval line 25
  3. def OAI.TwoPointCorrelations.PrimeMonomial.coefficientAt line 28
  4. def OAI.TwoPointCorrelations.PrimeMonomial.constantAt line 31
  5. lemma OAI.TwoPointCorrelations.PrimeMonomial.eval_affine line 34
  6. lemma OAI.TwoPointCorrelations.PrimeMonomial.eval_update_of_not_mem line 42
  7. lemma OAI.TwoPointCorrelations.PrimeMonomial.coefficientAt_update_self line 51
  8. lemma OAI.TwoPointCorrelations.PrimeMonomial.constantAt_update_self line 61
  9. lemma OAI.TwoPointCorrelations.PrimeMonomial.coefficientAt_update_of_not_mem line 68
  10. def OAI.TwoPointCorrelations.primeRelationEval line 84
  11. def OAI.TwoPointCorrelations.primeRelationCoefficient line 86
  12. def OAI.TwoPointCorrelations.primeRelationConstant line 89
  13. def OAI.TwoPointCorrelations.primeRelationContribution line 93

    Source documentation

    The contribution of precisely the terms containing this label.

    def primeRelationContribution (m : τ → PrimeMonomial ι) (i : ι) (x : ι → ℤ) : ℤ :=
…

    Mentions: OAI.TwoPointCorrelations.PrimeMonomial

  14. def OAI.TwoPointCorrelations.primeRelationSupport line 96
  15. lemma OAI.TwoPointCorrelations.primeRelation_affine line 98
  16. lemma OAI.TwoPointCorrelations.primeRelation_contribution_eq line 106
  17. lemma OAI.TwoPointCorrelations.primeRelation_coefficient_update_self line 117
  18. lemma OAI.TwoPointCorrelations.primeRelation_constant_update_self line 123
  19. lemma OAI.TwoPointCorrelations.primeRelation_update_affine line 129
  20. lemma OAI.TwoPointCorrelations.primeRelation_update_of_not_mem line 136
  21. lemma OAI.TwoPointCorrelations.primeRelation_coefficient_update_of_not_mem line 145
  22. lemma OAI.TwoPointCorrelations.primeRelation_coefficient_nondegenerate line 156

    Source documentation

    Retaining the nonzero-contribution test gives precisely the coefficient condition needed for a single-prime reciprocal saving.

    lemma primeRelation_coefficient_nondegenerate (m : τ → PrimeMonomial ι)
    (i : ι) (x : ι → ℤ) (p : ℤ)
    (hnonzero : ¬p ∣ primeRelationContribution m i x) :
    ¬p ∣ primeRelationCoefficient m i x := by
…

    Mentions: OAI.TwoPointCorrelations.PrimeMonomial, OAI.TwoPointCorrelations.primeRelationContribution, OAI.TwoPointCorrelations.primeRelationCoefficient

  23. def OAI.TwoPointCorrelations.primeRelationEvent line 167

    Source documentation

    The whole congruence, including its nondegeneracy test and controlling prime, ignores a variable outside the recorded support and control.

    def primeRelationEvent (m : τ → PrimeMonomial ι) (selected control : ι) (x : ι → ℤ) : Prop :=
…

    Mentions: OAI.TwoPointCorrelations.PrimeMonomial

  24. lemma OAI.TwoPointCorrelations.primeRelationEvent_update line 170