OAI/NumberTheory/TwoPoint/Bounds/PaddingPairSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The local three-boolean experiment agrees with first choosing all available primes and then independently choosing two padding divisors.

  1. def OAI.TwoPointCorrelations.paddingAvailableLaw line 13
  2. def OAI.TwoPointCorrelations.paddingDivisorLaw line 17
  3. def OAI.TwoPointCorrelations.paddingLog line 20
  4. def OAI.TwoPointCorrelations.paddingTripleEquiv line 23
  5. lemma OAI.TwoPointCorrelations.paddingPairLaw_weight line 30
  6. lemma OAI.TwoPointCorrelations.paddingPairLaw_average_nested line 40
  7. lemma OAI.TwoPointCorrelations.paddingPairDifference_value line 64
  8. theorem OAI.TwoPointCorrelations.padding_pair_difference_average line 75

    Source documentation

    Exact law of the difference of two conditionally sampled padding divisors.

    theorem padding_pair_difference_average (Q : Finset ℕ) (hQ : ∀ p ∈ Q, 2 ≤ p)
    (F : ℝ → ℝ) :
    (paddingAvailableLaw Q hQ).average (fun a =>
      (paddingDivisorLaw Q a).average (fun b =>
        (paddingDivisorLaw Q a).average (fun c => F (paddingLog Q b - paddingLog Q c)))) =
      (paddingDifferenceLaw Q hQ).average (fun x => F (paddingDifferenceValue Q x)) := by
…

    Mentions: OAI.TwoPointCorrelations.paddingAvailableLaw, OAI.TwoPointCorrelations.paddingDivisorLaw, OAI.TwoPointCorrelations.paddingLog, OAI.TwoPointCorrelations.paddingDifferenceLaw, OAI.TwoPointCorrelations.paddingDifferenceValue