OAI/NumberTheory/JointDickman/Arithmetic/PartialPrimeChannel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.partialFairPrimeTransition line 11
2. theorem OAI.JointDickman.partialFairPrimeTransition_nonneg line 15
3. theorem OAI.JointDickman.partialFairPrimeTransition_sum_le line 20
4. theorem OAI.JointDickman.partialFairPrimeTransition_marginal line 27
5. theorem OAI.JointDickman.partialFairPrimeKernel_independent_error line 45

   Source documentation

   The same actual two-split comparison applies when outputs outside all cells are discarded.

   theorem partialFairPrimeKernel_independent_error {A : Type*} [DecidableEq A]
       (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
       (hcut : ∀ p ∈ Q, N < p) (cell : ℕ → Option A) {m : ℝ} (hm : 0 < m) (a b : A) :
       |finiteTwoSplitKernel (fullPrimeMass Q) (fun _ => m) (partialFairPrimeTransition Q cell) a b -
         independentPairMass (quarterPrimeMass Q) (quarterPrimeMass Q)
           (primeProductCell Q cell) a b / (m * m)| ≤ (9 / (8 * N : ℝ)) / (m * m) := by
   …

   Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.partialFairPrimeTransition, OAI.JointDickman.independentPairMass, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeProductCell

6. theorem OAI.JointDickman.partialFairPrimeKernel_flat_error line 60

   Source documentation

   A local profile independent of the residue yields a flat retained kernel for the partial output channel.

   theorem partialFairPrimeKernel_flat_error {D R : Type*} [DecidableEq D] [DecidableEq R]
       (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
       (hcut : ∀ p ∈ Q, N < p) (cell : ℕ → Option (D × R))
       (low : (Q → Bool) → Prop) [DecidablePred low] (profile : (Q → Bool) → D → ℝ)
       {m η : ℝ} (hm : 0 < m) (hη : 0 ≤ η)
       (hlocal : ∀ c d r,
         |highExclusiveCell (quarterPrimeMass Q) (primeProductCell Q cell) low c (d, r) -
           profile c d| ≤ η) (d e : D) (r s : R) :
       |(finiteTwoSplitKernel (fullPrimeMass Q) (fun _ => m) (partialFairPrimeTransition Q cell)
           (d, r) (e, s) -
         lowUnionExclusiveKernel (quarterPrimeMass Q) (quarterPrimeMass Q)
           (primeProductCell Q cell) low (fun _ => m) (d, r) (e, s)) -
   …

   Mentions: OAI.JointDickman.highExclusiveCell, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeProductCell, OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.partialFairPrimeTransition, OAI.JointDickman.lowUnionExclusiveKernel

7. theorem OAI.JointDickman.partialFairPrimeResidueChannel_square_bound line 103

   Source documentation

   Residue centering for the actual channel with discarded outputs.

   theorem partialFairPrimeResidueChannel_square_bound {D R : Type*}
       [Fintype D] [Fintype R] [Nonempty R] [DecidableEq D] [DecidableEq R]
       (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
       (hcut : ∀ p ∈ Q, N < p) (cell : ℕ → Option (D × R))
       (low : (Q → Bool) → Prop) [DecidablePred low] (profile : (Q → Bool) → D → ℝ)
       {m H η : ℝ} (hm : 0 < m) (hH : 0 ≤ H) (hη : 0 ≤ η)
       (hmarginal : ∀ a, independentCellMarginal (quarterPrimeMass Q) (quarterPrimeMass Q)
         (primeProductCell Q cell) a ≤ H * m)
       (hcommon : ∀ e, low e → ∀ a,
         optionCellMass (quarterPrimeMass Q) (fun c => primeProductCell Q cell c e) a ≤ H * m)
       (hlocal : ∀ c d r,
         |highExclusiveCell (quarterPrimeMass Q) (primeProductCell Q cell) low c (d, r) -
   …

   Mentions: OAI.JointDickman.independentCellMarginal, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeProductCell, OAI.JointDickman.optionCellMass, OAI.JointDickman.highExclusiveCell