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

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

e.taum.prime.def (1121-1127), for m ≥ 1: τ'_m := (4⌈ε_{m-1}^{-δ}⌉ + 1)⁻¹ τ''_m. The value at m = 0 is unused.

Equations

• AVenhance.tauP β Λ m = (4 * ↑⌈AVenhance.epsilon β Λ (m - 1) ^ (-AVenhance.delta β)⌉₊ + 1)⁻¹ * AVenhance.tauPP β Λ m