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

noncomputable def AVenhance.psi (β : ℝ) (Λ m : ℕ) (k : ℤ) (x : Homogenization.Vec 2) : ℝ

e.def.streamr (1207-1210): ψ_{m,k} := a_m ε_m² ψ_{0,k}(· / ε_m), m ≥ 1.

Equations

• AVenhance.psi β Λ m k x = AVenhance.a β Λ m * AVenhance.epsilon β Λ m ^ 2 * AVenhance.psi0 k ((AVenhance.epsilon β Λ m)⁻¹ • x)