Statement file: tauPP (Ingredients). This file contains exactly one declaration of the formalization's public statement surface.

noncomputable def AVenhance.tauPP (β : ℝ) (Λ m : ℕ) : ℝ

e.taum.primeprime.def (1130-1136), for m ≥ 1: τ''_m := 2⁻²⁵ ⌈a_{m-1} / ε_{m-1}^{2δ}⌉⁻¹. The value at m = 0 is unused.

Equations

• AVenhance.tauPP β Λ m = 2 ^ (-25) * (↑⌈AVenhance.a β Λ (m - 1) / AVenhance.epsilon β Λ (m - 1) ^ (2 * AVenhance.delta β)⌉₊)⁻¹