TwoSplitKernelComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Operator comparison for the actual and independent two-split laws

The output cells may be any finite collection of sets of positive integers. Their common measure m is kept explicit. The estimates thus apply to the logarithm/residue cells in the paper without choosing a particular mesh.

def OAI.JointDickman.uniformProbabilityKernel line 18

theorem OAI.JointDickman.uniformProbabilityKernel_error line 23

Source documentation

A uniform cell probability error gives the corresponding square-norm operator error after division by the cell measures.

theorem uniformProbabilityKernel_error {A : Type*} [Fintype A]
    {m δ : ℝ} (hm : 0 < m) (hδ : 0 ≤ δ) (q r : A → A → ℝ)
    (hqr : ∀ a b, |q a b - r a b| ≤ δ) (g : A → ℝ) :
    (∑ a, m * (finiteKernelAction (fun _ => m)
      (fun a b => uniformProbabilityKernel m q a b - uniformProbabilityKernel m r a b) g a) ^ 2) ≤
      ((Fintype.card A : ℝ) * δ / m) ^ 2 * ∑ a, m * g a ^ 2 := by
…

Mentions: OAI.JointDickman.finiteKernelAction, OAI.JointDickman.uniformProbabilityKernel

def OAI.JointDickman.actualTwoSplitCellMass line 49
def OAI.JointDickman.independentTwoSplitCellMass line 55

theorem OAI.JointDickman.twoSplitKernel_error line 63

Source documentation

The two-split kernel replacement, for the actual prime products and any finite collection of output cells.

theorem twoSplitKernel_error {A : Type*} [Fintype A] (Q : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
    (hcut : ∀ p ∈ Q, N < p) (cells : A → Set ℕ) {m : ℝ} (hm : 0 < m)
    (g : A → ℝ) :
    (∑ a, m * (finiteKernelAction (fun _ => m)
      (fun a b => uniformProbabilityKernel m (actualTwoSplitCellMass Q cells) a b -
        uniformProbabilityKernel m (independentTwoSplitCellMass Q cells) a b) g a) ^ 2) ≤
      ((Fintype.card A : ℝ) * (9 / (8 * N : ℝ)) / m) ^ 2 * ∑ a, m * g a ^ 2 := by
…

Mentions: OAI.JointDickman.finiteKernelAction, OAI.JointDickman.uniformProbabilityKernel, OAI.JointDickman.actualTwoSplitCellMass, OAI.JointDickman.independentTwoSplitCellMass