Home

Chen proof dependencies

Arrows follow compiled declaration dependencies. Nodes marked (input) are introduced in another chapter. Click a node for its statement and Lean source.

Legend
Boxes
definitions
Ellipses
theorems and lemmas
Blue border
the statement of this result is ready to be formalized; all prerequisites are done
Orange border
the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background
the proof of this result is ready to be formalized; all prerequisites are done
Green border
the statement of this result is formalized
Green background
the proof of this result is formalized
Dark green background
the proof of this result and all its ancestors are formalized
Dark green border
this is in Mathlib
Inspect dependencies

Distribution closes the base lower bound · compiled type and proof/definition references.

Inspect dependencies

Subtract half the medium-prime upper bound · compiled type and proof/definition references.

Inspect dependencies

Chen finite counting inequality · compiled type and proof/definition references.

Inspect dependencies

Sum the conditioned finite upper sieves · compiled type and proof/definition references.

Inspect dependencies

Lower Rosser density gives the actual base sieve · compiled type and proof/definition references.

Inspect dependencies

Positive weight detects at most two factors · compiled type and proof/definition references.

Inspect dependencies

Bound the proper-prime-power correction · compiled type and proof/definition references.

Inspect dependencies

Chen: 0.67 representation bound · compiled type and proof/definition references.

Inspect dependencies

Expand the square into progression counts · compiled type and proof/definition references.

Inspect dependencies

Bound the optimized Selberg main term · compiled type and proof/definition references.

Inspect dependencies

A candidate prime contributes a unit Selberg packet · compiled type and proof/definition references.

Inspect dependencies

Pay the actual signed Selberg remainder · compiled type and proof/definition references.

Inspect dependencies

Pay the switched modulus weight by finite Cauchy · compiled type and proof/definition references.

Inspect dependencies

Chen prime plus at most two primes · compiled type and proof/definition references.

Inspect dependencies

Inject first-factor witnesses into source triples and endpoints · compiled type and proof/definition references.

Inspect dependencies

Chen triple-penalty upper bound · compiled type and proof/definition references.

Inspect dependencies

Close the varying-prime upper asymptotic · compiled type and proof/definition references.

Inspect dependencies

Chen weighted lower bound · compiled type and proof/definition references.

Inspect dependencies

Pay combined-modulus weighted prime errors · compiled type and proof/definition references.

Inspect dependencies

Bombieri–Vinogradov for primes · compiled type and proof/definition references.

Inspect dependencies

Constructed Jurkat--Richert comparison functions · compiled type and proof/definition references.

Inspect dependencies

Liu–Pan convolution distribution · compiled type and proof/definition references.

Inspect dependencies

Uniform dimension-one Goldbach local product · compiled type and proof/definition references.

Inspect dependencies

Mertens product with its identified constant · compiled type and proof/definition references.

Inspect dependencies

A quantitative prime number theorem · compiled type and proof/definition references.

Inspect dependencies

Asymptotic of the optimized Selberg denominator · compiled type and proof/definition references.

Inspect dependencies

Paying the signed Selberg remainder · compiled type and proof/definition references.

Inspect dependencies

Lower Rosser comparison uniform in the sieve · compiled type and proof/definition references.

Inspect dependencies

Modern upper Rosser comparison · compiled type and proof/definition references.

Inspect dependencies

The actual weighted conditioned Chen error · compiled type and proof/definition references.