OAI/NumberTheory/JointDickman/Amplification/SubsetPartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.subsetPartitionEquiv line 11
2. theorem OAI.JointDickman.bernoulliSubsetMass_union line 48
3. theorem OAI.JointDickman.bernoulliSubsetMass_partition_sum line 68

   Source documentation

   Arbitrary tests factor exactly after splitting the prime range.

   theorem bernoulliSubsetMass_partition_sum {α : Type*} [DecidableEq α]
       (P Q : Finset α) (hd : Disjoint P Q) (q : α → ℝ) (F : Finset α → ℝ) :
       (∑ S ∈ (P ∪ Q).powerset, bernoulliSubsetMass (P ∪ Q) q S * F S) =
         ∑ A ∈ P.powerset, ∑ D ∈ Q.powerset,
           bernoulliSubsetMass P q A * bernoulliSubsetMass Q q D * F (A ∪ D) := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass

4. theorem OAI.JointDickman.bernoulliSubsetMass_projection line 97

   Source documentation

   The selected high-range subset has its own Bernoulli law, independent of all choices in the complementary range.

   theorem bernoulliSubsetMass_projection {α : Type*} [DecidableEq α]
       (P Q D : Finset α) (hQ : Q ⊆ P) (hD : D ⊆ Q) (q : α → ℝ) :
       (∑ S ∈ P.powerset, if S ∩ Q = D then bernoulliSubsetMass P q S else 0) =
         bernoulliSubsetMass Q q D := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass