OAI/NumberTheory/JointDickman/Amplification/GeometricDiscardedArcs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original geometric sum loses only o(1/T) outside the retained arcs

  1. def OAI.JointDickman.geometricBoxIntegrand line 16

    Source documentation

    The lag is displayed separately from the geometric endpoint scale.

    noncomputable def geometricBoxIntegrand (B j : ℕ) (a b T t : ℝ)
    (g h : (auxiliaryPrimes B → Bool) → ℝ) (w₁ w₂ w₃ : ℝ → ℝ)
    (k : ℤ) (θ : ℝ) : ℂ :=
…

    Mentions: OAI.JointDickman.auxiliaryPrimes

  2. theorem OAI.JointDickman.geometric_discarded_arcs_vanishing line 23