OAI/NumberTheory/JointDickman/Arithmetic/PrimeDigitAverages.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Averaging the adaptive coefficient exceptions over prime digits

  1. theorem OAI.JointDickman.uniformZModMass_sum line 11
  2. theorem OAI.JointDickman.primeDigitMass_sum line 17
  3. def OAI.JointDickman.residuePrimePatterns line 21
  4. theorem OAI.JointDickman.residuePrimePatterns_arithmetic line 25
  5. theorem OAI.JointDickman.prime_square_crt_average line 31
  6. theorem OAI.JointDickman.primeDigit_conditional_bound line 57

    Source documentation

    The exposed observations may determine the entire candidate family.

    theorem primeDigit_conditional_bound {B M : ℕ}
    [∀ p : auxiliaryPrimes B, NeZero p.val]
    (F : BlockPrimePatterns B M → (∀ p : auxiliaryPrimes B, ZMod p.val) → ℝ)
    {K : ℝ} (hF : ∀ H, finiteExpectation (conditionalResidueMass H) (F H) ≤ K) :
    finiteExpectation (primeDigitMass B) (fun r => F (residuePrimePatterns r) r) ≤ K := by
…

    Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.BlockPrimePatterns, OAI.JointDickman.finiteExpectation, OAI.JointDickman.conditionalResidueMass, OAI.JointDickman.primeDigitMass, OAI.JointDickman.residuePrimePatterns

  7. theorem OAI.JointDickman.adaptive_masked_coefficient_probability line 80
  8. theorem OAI.JointDickman.adaptive_coefficient_digit_probability line 99