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

noncomputable def AVenhance.psi0 (k : ℤ) (x : Homogenization.Vec 2) : ℝ

e.def.streamr.0 (1194-1201): ψ_{0,k}(x) = sin(2π x_i) if k ∈ 4ℤ + 2i - 1, i ∈ {1,2} (coordinates x 0, x 1), and 0 for even k.

Equations

• AVenhance.psi0 k x = if k % 4 = 1 then Real.sin (2 * Real.pi * x 0) else if k % 4 = 3 then Real.sin (2 * Real.pi * x 1) else 0