HigherCharacterDecorrelation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Proposition 4.1: maximal translated higher-order bias has harmonic mass o(L)

def OAI.Ostmann.closedLogLogPrimeBand line 10
theorem OAI.Ostmann.mem_closedLogLogPrimeBand_iff line 14
def OAI.Ostmann.higherCharacterBandMass line 31
theorem OAI.Ostmann.PublishedProgressionInput.eventual_higher_character_mass_bound line 34

theorem OAI.Ostmann.PublishedProgressionInput.higher_character_decorrelation line 96

Source documentation

The manuscript's Proposition 4.1, with the maximum represented by the supremum over all translated characters whose square is nonprincipal.

theorem PublishedProgressionInput.higher_character_decorrelation
    (P0 : PublishedProgressionInput)
    (hsize : PublishedSummandSizeBound) {CM : ℝ} (hM : MertensEstimate CM)
    {Aset Bset : Set ℕ} (hAset : Aset.Infinite) (hBset : Bset.Infinite)
    (hsum : EventuallyPrimeSumset Aset Bset) (N₀ : ℕ)
    (hN₀ : ∀ p, p.Prime → Disjoint (tailResidues Aset N₀ p) (negTailResidues Bset N₀ p))
    (α β : ℝ) (hα : 0 < α) (hαβ : α < β) :
    (fun L => higherCharacterBandMass Aset N₀ α β L) =o[atTop] (fun L : ℝ => L) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedSummandSizeBound, OAI.Ostmann.MertensEstimate, OAI.Ostmann.EventuallyPrimeSumset, OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.higherCharacterBandMass