1
Bombieri–Vinogradov
▶
1.1
Statement
1.2
Assumptions
1.3
Definitions
1.4
Reduction to \(\Delta _\Lambda \)
1.5
Vaughan’s Identity
1.6
Small Primes (\(\Lambda _{\le U}\))
1.7
Type I Sums (\(\Lambda ^\sharp \))
1.8
Type II Sums (\(\Lambda ^\flat \))
▶
1.8.1
Definitions
1.8.2
Reduction to character sums
1.8.3
Large sieve estimates
Dependency graph
Formalizing Bombieri Vinogradov
Arend Mellendijk
1
Bombieri–Vinogradov
1.1
Statement
1.2
Assumptions
1.3
Definitions
1.4
Reduction to \(\Delta _\Lambda \)
1.5
Vaughan’s Identity
1.6
Small Primes (\(\Lambda _{\le U}\))
1.7
Type I Sums (\(\Lambda ^\sharp \))
1.8
Type II Sums (\(\Lambda ^\flat \))
1.8.1
Definitions
1.8.2
Reduction to character sums
1.8.3
Large sieve estimates