Lemma U: Parseval as a limit, and the low/high eigenvalue thresholds

theorem AVenhance.Infra.FullTheorem.LemmaU.sum_cellCoeff_sq_tendsto {d : Homogenization.Vec 2 → ℝ} (hd : Homogenization.MemL2On unitCube d) : Filter.Tendsto (fun (M : ℕ) => ∑ a : Parabolic.FourierGalerkin.RealFourierIndex M, cellCoeff M d a ^ 2) Filter.atTop (nhds (l2NormSq d))

Parseval: the sum of squared cell coefficients converges to the squared L² norm.

theorem AVenhance.Infra.FullTheorem.LemmaU.modeLam_le_of_low (M : ℕ) (K : ℝ) (a : Parabolic.FourierGalerkin.RealFourierIndex M) (h : ∀ (i : Fin 2), |Classical.realFourierModeDerivativeScale a i| ≤ 2 * Real.pi * K) : modeLam M a ≤ 80 * K ^ 2

Low modes: the eigenvalue is at most 80 K².

theorem AVenhance.Infra.FullTheorem.LemmaU.modeLam_ge_of_high (M : ℕ) {K : ℝ} (hK : 0 ≤ K) (a : Parabolic.FourierGalerkin.RealFourierIndex M) (h : ¬∀ (i : Fin 2), |Classical.realFourierModeDerivativeScale a i| ≤ 2 * Real.pi * K) : 36 * K ^ 2 ≤ modeLam M a

High modes: the eigenvalue is at least 36 K².