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

def AVenhance.IsPeriodicH1 (u : Homogenization.Vec 2 → ℝ) : Prop

Periodic H¹(𝕋²).

Equations

• AVenhance.IsPeriodicH1 u = ∃ (Du : Homogenization.Vec 2 → Homogenization.Vec 2), AVenhance.IsPeriodicH1With u Du