Documentation

MathlibNt.SieveTheory.LiLiuGoldbachOrdinaryLowerDensityFactors

source
theorem MathlibNt.SieveTheory.continuousLowerFactor_eq_jr1965f {s : ℝ} (hs : 2 ≤ s) :
suzukiContinuousLowerFactor s = JurkatRichert1965ChenGammaOneQOne.jr1965f s

The full legal continuous lower factor is the constructed JR lower function.

Inspect dependencies

MathlibNt.SieveTheory.continuousLowerFactor_eq_jr1965f · compiled type and proof/definition references.

source
theorem MathlibNt.SieveTheory.jr1965f_eq_first_log {s : ℝ} (hs2 : 2 ≤ s) (hs4 : s ≤ 4) :
JurkatRichert1965ChenGammaOneQOne.jr1965f s = 2 * Real.exp Real.eulerMascheroniConstant * Real.log (s - 1) / s

The first interval formula, with the same constructed source and amplitude.

Inspect dependencies

MathlibNt.SieveTheory.jr1965f_eq_first_log · compiled type and proof/definition references.