Spatial difference identities for classical periodic solutions.
theorem
AVenhance.Infra.Classical.smooth_spaceGrad_sub
{f g : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hg : ContDiff ℝ (↑⊤) g)
:
(spaceGrad fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) =>
spaceGrad f x - spaceGrad g x
theorem
AVenhance.Infra.Classical.smooth_spaceLap_sub
{f g : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hg : ContDiff ℝ (↑⊤) g)
:
(spaceLap fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => spaceLap f x - spaceLap g x
theorem
AVenhance.Infra.Classical.continuous_integrableOn_unitCellAt
{f : Homogenization.Vec 2 → ℝ}
(a : Homogenization.Vec 2)
(hf : Continuous f)
: