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

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

⟨f⟩ = ⨍_{𝕋²} f dx (line 921), as the integral over the open unit cube (|𝕋²| = 1).

Equations

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