PrimeMassApproximation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Removing the local odds correction from prime-product masses

For every event, the independent-subset mass differs from the uncorrected Euler weight by at most the sum of squared selection probabilities. The resulting prime-tail error is uniform over events.

def OAI.JointDickman.uncorrectedSubsetMass line 18
theorem OAI.JointDickman.uncorrectedSubsetMass_identity line 21
theorem OAI.JointDickman.uncorrectedSubsetMass_le line 27
theorem OAI.JointDickman.uncorrectedSubsetMass_sum line 36
theorem OAI.JointDickman.one_sub_prod_le_sum line 46
theorem OAI.JointDickman.uncorrectedSubsetMass_event_error line 58

theorem OAI.JointDickman.primeSubsetMass_event_error line 88

Source documentation

The local mass correction is uniformly small without any restriction on the event or on the size of the selected prime product.

theorem primeSubsetMass_event_error (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    {N : ℕ} (hN : N ≠ 0) (hcut : ∀ p ∈ P, N < p)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1) (E : Finset ℕ → Prop) :
    |(∑ S ∈ P.powerset, if E S then bernoulliSubsetMass P (fun p => z / p) S else 0) -
      (∑ S ∈ P.powerset, if E S then uncorrectedSubsetMass P (fun p => z / p) S else 0)| ≤
      z ^ 2 / (N : ℝ) := by
…

Mentions: OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.uncorrectedSubsetMass