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

noncomputable def AVenhance.l2NormSq (f : Homogenization.Vec 2 → ℝ) : ℝ

∫_{(0,1)²} f².

Equations

• AVenhance.l2NormSq f = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, f x ^ 2