HighExclusiveLocalLaw.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local laws for the high-exclusive part of the actual prime channel

def OAI.JointDickman.lowPrimeLog line 12
def OAI.JointDickman.clippedIntervalIntegral line 16
theorem OAI.JointDickman.highExclusiveLogCell_eq line 20

theorem OAI.JointDickman.highExclusiveLogCell_local_law line 52

Source documentation

The retained exclusive cell is approximated by a residue-independent integral, uniformly even for a partial cell at the high cutoff.

theorem highExclusiveLogCell_local_law
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ v : ℕ → ℝ, v 0 = squarefreeLeadingConstant (1 / 4) ∧ 0 < v 0 ∧
      ∃ H : ℕ, ∃ C : ℝ, 0 < C ∧ ∀ᶠ B : ℕ in atTop,
        ∀ (D : Type*) [DecidableEq D], ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
        ∀ lower upper : D → ℝ,
        (∀ d e s, s ∈ Set.Ioc (lower d) (upper d) → s ∈ Set.Ioc (lower e) (upper e) → d = e) →
        (∀ d, upper d ≤ 16 / 5) → ∀ c : auxiliaryPrimes B → Bool, ∀ d : D, ∀ r : (ZMod q)ˣ,
        |highExclusiveCell (quarterPrimeMass (auxiliaryPrimes B))
            (primeProductCell (auxiliaryPrimes B) (logResidueCell B q lower upper))
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.highExclusiveCell, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeProductCell, OAI.JointDickman.logResidueCell