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

noncomputable def AVenhance.spaceTimeGradNormSq (Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ

The squared space-time norm ‖∇θ‖²_{L²((0,1)×𝕋²)} of a weak gradient Dθ.

Equations

• AVenhance.spaceTimeGradNormSq Dθ = ∫ (p : ℝ × Homogenization.Vec 2) in AVenhance.timeCube, Homogenization.vecNormSq (Dθ p.1 p.2)