OAI/NumberTheory/TwoPoint/Walks/ColumnCoefficientBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Concrete fixed-column coefficients and the size hypothesis for random-prime rank.

  1. def OAI.TwoPointCorrelations.SignedStep.columnCoefficient line 13
  2. lemma OAI.TwoPointCorrelations.SignedStep.displacement_eq_columnCoefficient line 18

    Source documentation

    Once the other columns are fixed, the coefficient contains no prime variable from the resampled column.

    lemma displacement_eq_columnCoefficient (a : SignedStep) (h p other : ℕ)
    (htuple : a.tuple = p * other) :
    a.displacement h = a.columnCoefficient h other * p := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep

  3. lemma OAI.TwoPointCorrelations.SignedStep.abs_columnCoefficient line 24
  4. lemma OAI.TwoPointCorrelations.integerColumnDeparture_abs_sum_le line 32
  5. lemma OAI.TwoPointCorrelations.columnDifference_abs_sum_le line 47
  6. lemma OAI.TwoPointCorrelations.columnDifference_abs_sum_le_uniform line 64
  7. lemma OAI.TwoPointCorrelations.abs_primeDifference_le line 83
  8. lemma OAI.TwoPointCorrelations.primeDifference_natAbs_le line 112