OAI/NumberTheory/TwoPoint/Bounds/PaddingDifferenceLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual independent three-point padding difference law and its characteristic product. At each prime the two nonzero atoms have the manuscript's exact probability 4/(5(p+4)).

  1. def OAI.TwoPointCorrelations.paddingDifferenceAtom line 16
  2. def OAI.TwoPointCorrelations.paddingDifferenceStep line 19
  3. def OAI.TwoPointCorrelations.paddingStepLaw line 22
  4. def OAI.TwoPointCorrelations.paddingDifferenceLaw line 37
  5. def OAI.TwoPointCorrelations.paddingDifferenceValue line 41
  6. lemma OAI.TwoPointCorrelations.paddingStep_characteristic line 44
  7. theorem OAI.TwoPointCorrelations.paddingDifference_characteristic line 61

    Source documentation

    The complete finite-law characteristic function is the real, nonnegative product estimated in PaddingCharacteristic.

    theorem paddingDifference_characteristic (Q : Finset ℕ) (hQ : ∀ p ∈ Q, 2 ≤ p) (t : ℝ) :
    (∑ x : Q → Fin 3, ((paddingDifferenceLaw Q hQ).weight x : ℂ) *
      Complex.exp (((t * paddingDifferenceValue Q x : ℝ) : ℂ) * Complex.I)) =
        (paddingCharacteristic Q t : ℂ) := by
…

    Mentions: OAI.TwoPointCorrelations.paddingDifferenceLaw, OAI.TwoPointCorrelations.paddingDifferenceValue, OAI.TwoPointCorrelations.paddingCharacteristic

  8. lemma OAI.TwoPointCorrelations.paddingDifference_cosine line 81