OAI/NumberTheory/JointDickman/Arithmetic/RequiredPrimeSubset.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.bernoulliSubsetMass_required line 11
2. theorem OAI.JointDickman.independent_site_contains_prime_product line 60

   Source documentation

   For the independent 1/p law, a fixed squarefree coefficient is available at an additional endpoint with probability exactly its reciprocal.

   theorem independent_site_contains_prime_product (P A : Finset ℕ) (hA : A ⊆ P) :
       (∑ S ∈ P.powerset, if A ⊆ S then
         bernoulliSubsetMass P (fun p => 1/(p : ℝ)) S else 0) =
           1/(∏ p ∈ A, p : ℕ) := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass