OAI/NumberTheory/JointDickman/Amplification/SignedPairPushforward.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.signedSplitProductMass_zero_off_support line 11
2. theorem OAI.JointDickman.signedSplitProductMass_sum_on line 28
3. theorem OAI.JointDickman.signedSplitProductMass_pair_expectation line 41
4. theorem OAI.JointDickman.primeProductMass_sum_test line 83

   Source documentation

   The unsigned law pushed to products, retaining an arbitrary test.

   theorem primeProductMass_sum_test (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (z : ℝ) (F : ℕ → ℝ) :
       (∑ n ∈ primeSplitProductSupport P, primeProductMass P z n*F n) =
         ∑ A ∈ P.powerset, bernoulliSubsetMass P (fun p => z/p) A*F (∏ p ∈ A,p) := by
   …

   Mentions: OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.primeProductMass, OAI.JointDickman.bernoulliSubsetMass