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

noncomputable def AVenhance.spaceAvgMat (F : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Entrywise ⟨F⟩ for a 2×2-matrix valued periodic function of space.

Equations

• AVenhance.spaceAvgMat F = Matrix.of fun (i j : Fin 2) => AVenhance.spaceAvg fun (x : Homogenization.Vec 2) => F x i j