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

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

e.am.def (1094): a_m := ε_m^{β-2}.

Equations

• AVenhance.a β Λ m = AVenhance.epsilon β Λ m ^ (β - 2)