Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.StandardBVHighConductorLocalAssembly

Scalar Pan-cutoff payment for conductor-local high ledgers #

This is the terminal scalar part of the high-source assembly. All shell, prefix-maximal, harmonic, and coefficient losses may be collected into a fixed power log(N)^κ. The conductor exponent pays the N/√R lane and Pan's modulus exponent pays the Q√N lane independently.

source
def AnalyticNumberTheory.LargeSieve.conductorLocalPanConductorExponent (A κ : ℕ) :
ℕ

The choices used by the high-conductor scalar payment.

Equations
Instances For
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.conductorLocalPanConductorExponent · compiled type and proof/definition references.

    source
    def AnalyticNumberTheory.LargeSieve.conductorLocalPanModulusExponent (A κ : ℕ) :
    ℕ
    Equations
    Instances For
      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.conductorLocalPanModulusExponent · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.conductorLocal_high_scales_pan_payable (A κ : ℕ) :
      ∀ᶠ (N : ℕ) in Filter.atTop, have C := conductorLocalPanConductorExponent A κ; have B := conductorLocalPanModulusExponent A κ; have R := logConductorThreshold N C; have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; Real.log ↑N ^ κ * (↑N / √↑R + ↑Q * √↑N) ≤ 2 * ↑N / Real.log ↑N ^ A

      Complete scalar payment. This theorem has no analytic premise: it proves that the two scales delivered by the conductor-local square ledgers fit the Standard-BV target after one fixed polylogarithmic shell loss.

      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.conductorLocal_high_scales_pan_payable · compiled type and proof/definition references.