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

def AVenhance.permittedInterval (β : ℝ) (Λ M : ℕ) : Set ℝ

e.permitted (label 3564): the interval [½ ε_M^{2β/(q+1)}, 2 ε_M^{2β/(q+1)}].

Equations

• AVenhance.permittedInterval β Λ M = Set.Icc (1 / 2 * AVenhance.epsilon β Λ M ^ (2 * β / (AVenhance.q β + 1))) (2 * AVenhance.epsilon β Λ M ^ (2 * β / (AVenhance.q β + 1)))