OAI/NumberTheory/JointDickman/Amplification/ThinningRanges.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.sum_powerset_partition line 11
2. theorem OAI.JointDickman.subsetRetentionMass_union line 23
3. def OAI.JointDickman.jointRetentionMass line 46
4. theorem OAI.JointDickman.jointRetentionMass_union line 50
5. theorem OAI.JointDickman.jointRetentionMass_partition line 61

   Source documentation

   The joint law factors before imposing any event. This keeps the order of high-prime exposure and low-prime averaging explicit.

   theorem jointRetentionMass_partition {α : Type*} [DecidableEq α]
       (P Q : Finset α) (hd : Disjoint P Q) (q : α → ℝ) (F : Finset α → Finset α → ℝ) :
       (∑ S ∈ (P ∪ Q).powerset, ∑ T ∈ (P ∪ Q).powerset,
         jointRetentionMass (P ∪ Q) q S T * F S T) =
         ∑ S ∈ P.powerset, ∑ R ∈ Q.powerset, ∑ U ∈ P.powerset, ∑ V ∈ Q.powerset,
           jointRetentionMass P q S U * jointRetentionMass Q q R V * F (S ∪ R) (U ∪ V) := by
   …

   Mentions: OAI.JointDickman.jointRetentionMass

6. theorem OAI.JointDickman.remaining_high_no_addition_bound line 83

   Source documentation

   A lower bound on the number of exposed remaining primes bounds the chance that none of their fair second coins adds a prime.

   theorem remaining_high_no_addition_bound {α : Type*} [DecidableEq α]
       (P : Finset α) (q : α → ℝ) (k : ℝ)
       (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1) :
       (∑ S ∈ P.powerset, if k ≤ (S.card : ℝ) then jointRetentionMass P q S ∅ else 0) ≤
         (1 / 2 : ℝ)^k := by
   …

   Mentions: OAI.JointDickman.jointRetentionMass