OAI/NumberTheory/JointDickman/Arithmetic/PrimeSiteBridge.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.selectedPrimeSubset line 12
2. theorem OAI.JointDickman.selectedPrimeSubset_mem line 15
3. theorem OAI.JointDickman.selectedPrimeSubset_subset line 19
4. theorem OAI.JointDickman.selectedPrimeSubset_injective line 22
5. theorem OAI.JointDickman.selectedPrimeSubset_surjective line 30
6. theorem OAI.JointDickman.retainedPrimeProduct_selected line 39
7. theorem OAI.JointDickman.bernoulliSiteMass_selected line 54
8. theorem OAI.JointDickman.bernoulliPrimeSite_event line 75

   Source documentation

   This equality transfers every event, not just an interval or a residue class.

   theorem bernoulliPrimeSite_event (Q : Finset ℕ) (q : ℕ → ℝ) (A : ℕ → Prop) :
       (∑ x : Q → Bool, if A (retainedPrimeProduct Q x) then
         bernoulliSiteMass (fun p : Q => q p.val) x else 0) =
         ∑ S ∈ Q.powerset, if A (∏ p ∈ S, p) then bernoulliSubsetMass Q q S else 0 := by
   …

   Mentions: OAI.JointDickman.retainedPrimeProduct, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.bernoulliSubsetMass

9. theorem OAI.JointDickman.quarterPrimeMass_small_log_tail line 91
10. theorem OAI.JointDickman.primeSiteMass_event line 117
11. theorem OAI.JointDickman.quarterPrimeMass_eq line 125
12. theorem OAI.JointDickman.retainedPrimeProduct_pos line 132
13. theorem OAI.JointDickman.retainedPrimeProduct_coprime line 137