OAI/NumberTheory/JointDickman/Arithmetic/PrimeResidueChannel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.fullPrimeMass line 18
2. def OAI.JointDickman.quarterPrimeMass line 21
3. def OAI.JointDickman.fairPrimeTransition line 24
4. def OAI.JointDickman.primeOutputCell line 28
5. theorem OAI.JointDickman.fullPrimeMass_nonneg line 32
6. theorem OAI.JointDickman.quarterPrimeMass_nonneg line 41
7. theorem OAI.JointDickman.quarterPrimeMass_sum line 51
8. theorem OAI.JointDickman.fairPrimeKernel_independent_error line 56

   Source documentation

   The actual fair-split channel kernel and the independent triple kernel are compared through their real cell-pair probabilities.

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

   Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.fairPrimeTransition, OAI.JointDickman.independentPairMass, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeOutputCell

9. def OAI.JointDickman.primeLowUnionKernel line 91

   Source documentation

   The nonnegative part discarded from the independent model.

   noncomputable def primeLowUnionKernel {A : Type*} [DecidableEq A]
       (Q : Finset ℕ) (cell : ℕ → A) (low : (Q → Bool) → Prop) [DecidablePred low]
       (m : ℝ) : A → A → ℝ :=
   …

10. def OAI.JointDickman.primeHighExclusiveCell line 97
11. theorem OAI.JointDickman.fairPrimeKernel_discarded_flat_error line 104

    Source documentation

    The actual kernel minus the independent low union is uniformly flat, with the explicit local-law and prime-comparison errors added together.

    theorem fairPrimeKernel_discarded_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 : ℕ → D × R)
        (low : (Q → Bool) → Prop) [DecidablePred low] (profile : (Q → Bool) → D → ℝ)
        {m η : ℝ} (hm : 0 < m) (hη : 0 ≤ η)
        (hlocal : ∀ c d r, |primeHighExclusiveCell Q cell low c (d, r) - profile c d| ≤ η)
        (d e : D) (r s : R) :
        |(finiteTwoSplitKernel (fullPrimeMass Q) (fun _ => m) (fairPrimeTransition Q cell)
              (d, r) (e, s) - primeLowUnionKernel Q cell low m (d, r) (e, s)) -
            flatExclusiveKernel (quarterPrimeMass Q) (fun _ => m) profile d e| ≤
          (2 * η + η ^ 2) / (m * m) + (9 / (8 * N : ℝ)) / (m * m) := by
    …

    Mentions: OAI.JointDickman.primeHighExclusiveCell, OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.fairPrimeTransition, OAI.JointDickman.primeLowUnionKernel, OAI.JointDickman.flatExclusiveKernel, OAI.JointDickman.quarterPrimeMass

12. theorem OAI.JointDickman.fairPrimeResidueChannel_square_bound line 147

    Source documentation

    The complete finite residue-channel estimate. All analytic information is isolated in the genuine marginal, common-cell and high-exclusive local bounds; the kernel identities and operator estimate are proved here.

    theorem fairPrimeResidueChannel_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 : ℕ → 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)
          (primeOutputCell Q cell) a ≤ H * m)
        (hcommon : ∀ e, low e → ∀ a,
          optionCellMass (quarterPrimeMass Q) (fun c => primeOutputCell Q cell c e) a ≤ H * m)
        (hlocal : ∀ c d r, |primeHighExclusiveCell Q cell low c (d, r) - profile c d| ≤ η)
        (f : (Q → Bool) → ℝ) :
    …

    Mentions: OAI.JointDickman.independentCellMarginal, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeOutputCell, OAI.JointDickman.optionCellMass, OAI.JointDickman.primeHighExclusiveCell