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

noncomputable def AVenhance.gradNormSq (Du : Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ

∫_{(0,1)²} |Du|² (Euclidean length of the gradient).

Equations

• AVenhance.gradNormSq Du = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, Homogenization.vecNormSq (Du x)