OAI/NumberTheory/JointDickman/Arithmetic/PrimeMarginalComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.independentPrimeCellMass_eq_marginal line 12
2. theorem OAI.JointDickman.independentPrimeMarginal_fair_error line 45

   Source documentation

   The two-split comparison already controls the one-coordinate marginal; no new coupling assumption is needed.

   theorem independentPrimeMarginal_fair_error {A : Type*} [DecidableEq A]
       (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
       (hcut : ∀ p ∈ Q, N < p) (cell : ℕ → Option A) (a : A) :
       |independentCellMarginal (quarterPrimeMass Q) (quarterPrimeMass Q)
           (primeProductCell Q cell) a -
         optionCellMass (bernoulliSiteMass (fun p : Q => 1 / (2 * (p.val : ℝ))))
           (fun y => cell (retainedPrimeProduct Q y)) a| ≤ 9 / (8 * N : ℝ) := by
   …

   Mentions: OAI.JointDickman.independentCellMarginal, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeProductCell, OAI.JointDickman.optionCellMass, OAI.JointDickman.bernoulliSiteMass, OAI.JointDickman.retainedPrimeProduct