Smooth periodic functions are periodic H¹

A C¹ periodic function is in the periodic H¹ class with its classical gradient.

theorem AVenhance.Infra.Section5.RelativeError.spaceGrad_continuous_of_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

Coordinates of the classical gradient of a C¹ function are continuous.

theorem AVenhance.Infra.Section5.RelativeError.isPeriodicH1With_of_contDiff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hp : IsZ2Periodic f) : IsPeriodicH1With f fun (x : Homogenization.Vec 2) => spaceGrad f x

A C¹ periodic function is periodic H¹ with its classical gradient.