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

def AVenhance.permissibleSet (β : ℝ) (Λ : ℕ) : Set ℝ

e.permissible.K (label 3550): 𝒦 = ⋃_{m ∈ ℕ} [½ ε_m^{2β/(q+1)}, 2 ε_m^{2β/(q+1)}].

Equations

• AVenhance.permissibleSet β Λ = ⋃ (M : ℕ), ⋃ (_ : 1 ≤ M), AVenhance.permittedInterval β Λ M

5. The PDE definition of the correctors and its well-posedness (flagged: source says

"the solution", e.parabcorr.k, label 2791)