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

noncomputable def AVenhance.delta (β : ℝ) : ℝ

e.delta (1008): δ := (1/4)(q-1)(1 - ((2q+1)/(2q+2)) β).

Equations

• AVenhance.delta β = 1 / 4 * (AVenhance.q β - 1) * (1 - (2 * AVenhance.q β + 1) / (2 * AVenhance.q β + 2) * β)