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

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

e.taum.def (1108-1116): τ_0 := 1, and for m ≥ 1, τ_m := (4⌈ε_{m-1}^{-δ}⌉ + 1)⁻² τ''_m.

Equations

• AVenhance.tau β Λ m = if m = 0 then 1 else (4 * ↑⌈AVenhance.epsilon β Λ (m - 1) ^ (-AVenhance.delta β)⌉₊ + 1)⁻¹ ^ 2 * AVenhance.tauPP β Λ m