OAI/NumberTheory/JointDickman/Arithmetic/RequiredPrimeProduct.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Availability of a prescribed coefficient at an independent endpoint

  1. def OAI.JointDickman.PrimeProductAvailable line 10
  2. theorem OAI.JointDickman.independent_site_available_le line 16

    Source documentation

    A prescribed integer is available with probability 1/n if it is a squarefree product of the allowed primes, and probability zero otherwise.

    theorem independent_site_available_le (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (n : ℕ) :
    (∑ S ∈ P.powerset, if PrimeProductAvailable n S then
      bernoulliSubsetMass P (fun p => 1/(p : ℝ)) S else 0) ≤ 1/(n : ℝ) := by
…

    Mentions: OAI.JointDickman.PrimeProductAvailable, OAI.JointDickman.bernoulliSubsetMass

  3. theorem OAI.JointDickman.independent_site_large_available_le line 48