OAI/NumberTheory/JointDickman/Arithmetic/OccupiedPrimeMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal mass of occupied primes in independent endpoint sites

  1. theorem OAI.JointDickman.finiteExpectation_finset_sum line 11
  2. def OAI.JointDickman.occupiedPrimeReciprocalMass line 19
  3. theorem OAI.JointDickman.independent_site_prime_hit line 23
  4. theorem OAI.JointDickman.independent_occupied_prime_probability line 43
  5. theorem OAI.JointDickman.independent_occupied_prime_mass line 58

    Source documentation

    The candidate family need not be independent of occupied primes: this estimate controls their entire reciprocal mass before using its deterministic candidate-count bound.

    theorem independent_occupied_prime_mass (B M : ℕ) :
    finiteExpectation (siteProductMass (fun _ : Fin M => independentPrimeSetMass B))
      (fun S => occupiedPrimeReciprocalMass B (fun i => (S i).val)) ≤
      (M : ℝ)*(∑ p ∈ auxiliaryPrimes B, 1/(p : ℝ)^2) := by
…

    Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.independentPrimeSetMass, OAI.JointDickman.occupiedPrimeReciprocalMass, OAI.JointDickman.auxiliaryPrimes