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

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

Χ^κ_m := ∑_{k ∈ ℤ} ξ_{m,k} Χ^κ_{m,k}, e.Chim (label 2909).

Equations

• I.chiM κ m t x = ∑' (k : ℤ), I.xiMK m k t • I.chiMK κ m k t x