HighExclusiveThreshold.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

High-exclusive local law for fixed smoothing thresholds

theorem OAI.JointDickman.highExclusiveLogCell_threshold_law line 15

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_threshold_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 : ℝ) →
        ∀ θ : ℝ, (B : ℝ) ^ (-(1 / 10 : ℝ)) ≤ θ →
        ∀ 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))
…

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