SmoothPrincipalMean.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The principal term of the smooth character estimate

Published input: the conductor-one case of Montgomery–Vaughan (2007), Corollary 11.20, equations (11.32)/(11.34), p.381, with the usual smooth partial summation. This is the classical prime number theorem with its zero-free-region error, specialized to our single fixed compactly supported smooth function. It makes no assertion about a growing character family.

def OAI.Ostmann.smoothPrincipalMain line 17
def OAI.Ostmann.smoothPrincipalError line 20
def OAI.Ostmann.PublishedSmoothPrincipalPNT line 24
Source documentation
The fixed-test, conductor-one consequence of the classical PNT.
```
def PublishedSmoothPrincipalPNT : Prop :=
…
```
theorem OAI.Ostmann.smooth_principal_decay line 28

theorem OAI.Ostmann.smooth_primitive_family_decay line 62

Source documentation

Lemma 5.3, including the conductor-one term.

theorem smooth_primitive_family_decay (Z : ∀ χ, ComplexZeroEnumeration χ)
    (hD : PublishedComplexZeroDensity Z) (hR : PublishedComplexZeroRegion Z)
    (P : PublishedSmoothExplicitFormula Z) (hPNT : PublishedSmoothPrincipalPNT)
    (a D : ℝ) (ha : 0 < a) :
    ∀ᶠ L : ℝ in atTop, ∀ Q : ℕ, 101 ≤ Q →
      L ^ 2 ≤ Real.log Q → Real.log Q ≤ a * L * Real.exp ((9 / 10 : ℝ) * L) →
      ∃ exception : Option PrimitiveComplexCharacter,
      ∀ F : Finset PrimitiveComplexCharacter,
        (∀ χ ∈ F, χ.modulus ≤ Q) → (∀ χ ∈ F, some χ ≠ exception) →
        smoothPrincipalError (Real.exp (Real.exp L)) +
          (∑ χ ∈ F, ‖smoothMangoldtMean χ.modulus χ.character (Real.exp (Real.exp L))‖) ≤
          Real.exp (Real.exp L) * Real.exp (-D * L) := by
…

Mentions: OAI.Ostmann.ComplexZeroEnumeration, OAI.Ostmann.PublishedComplexZeroDensity, OAI.Ostmann.PublishedComplexZeroRegion, OAI.Ostmann.PublishedSmoothExplicitFormula, OAI.Ostmann.PublishedSmoothPrincipalPNT, OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.smoothPrincipalError, OAI.Ostmann.smoothMangoldtMean