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

noncomputable def AVenhance.Ingredients.psiM {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

ψ_m(t, x) := ∑_{k ∈ 2ℤ+1} ζ̂_{m,l_k}(t) ζ_{m,k}(t) ψ_{m,k}(x), e.psi.m (label 2755).

Equations

• I.psiM m t x = ∑' (k : { k : ℤ // Odd k }), I.zetaProd m (↑k) t * AVenhance.psi β I.Λ m (↑k) x