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

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

Laplacian Δf = ∑_i ∂_i ∂_i f.

Equations

• AVenhance.spaceLap f x = ∑ i : Fin 2, AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => AVenhance.spaceGrad f y i) x i