theorem
LiLiuBuchstabSharp.buchstab_sharp_window_closed
{u : ℝ}
(hu : 17 / 4 ≤ u)
(hu' : u ≤ 21 / 4)
:
The actual Buchstab function on the entire starting unit window.
Inspect dependencies
LiLiuBuchstabSharp.buchstab_sharp_window_closed · compiled type and proof/definition references.
Requested sharp upper bound for the actual Buchstab function on the full tail. This only consumes the pre-existing tail-propagation theorem.
Inspect dependencies
LiLiuBuchstabSharp.buchstab_sharp_tail_closed · compiled type and proof/definition references.