HDot⁻¹ duality for a smooth periodic test function

If hMinusOneNorm h is finite then |∫ h w| ≤ ‖h‖_{HDot⁻¹} · ‖∇w‖_{L²} for every smooth periodic w; in the degenerate case ∇w = 0 this forces ∫ h w = 0 (constants are admissible tests, so ‖h‖_{HDot⁻¹} would otherwise be infinite).

theorem AVenhance.Infra.Section5.Integration.Energy.measurableSet_unitCube : MeasurableSet unitCube

theorem AVenhance.Infra.Section5.Integration.Energy.spaceGrad_const_mul {w : Homogenization.Vec 2 → ℝ} (hw : ContDiff ℝ (↑⊤) w) (c : ℝ) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * w y) x = fun (i : Fin 2) => c * spaceGrad w x i

theorem AVenhance.Infra.Section5.Integration.Energy.gradNormSq_nonneg (D : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq D

theorem AVenhance.Infra.Section5.Integration.Energy.gradNormSq_const_mul {w : Homogenization.Vec 2 → ℝ} (hw : ContDiff ℝ (↑⊤) w) (c : ℝ) : gradNormSq (spaceGrad fun (y : Homogenization.Vec 2) => c * w y) = c ^ 2 * gradNormSq (spaceGrad w)

theorem AVenhance.Infra.Section5.Integration.Energy.scaled_pairing_le {h w : Homogenization.Vec 2 → ℝ} (hw : ContDiff ℝ (↑⊤) w) (hper : IsZ2Periodic w) (hfin : hMinusOneNorm h ≠ ⊤) {c : ℝ} (hc : 0 ≤ c) (hcG : c ^ 2 * gradNormSq (spaceGrad w) ≤ 1) : c * |∫ (x : Homogenization.Vec 2) in unitCube, h x * w x| ≤ (hMinusOneNorm h).toReal

A scalar multiple of an admissible-up-to-scaling smooth periodic function is a test, giving the basic inequality λ |∫ h w| ≤ ‖h‖_{HDot⁻¹} whenever λ ‖∇w‖ ≤ 1.

theorem AVenhance.Infra.Section5.Integration.Energy.abs_integral_mul_le_hMinusOneNorm {h w : Homogenization.Vec 2 → ℝ} (hw : ContDiff ℝ (↑⊤) w) (hper : IsZ2Periodic w) (hfin : hMinusOneNorm h ≠ ⊤) : |∫ (x : Homogenization.Vec 2) in unitCube, h x * w x| ≤ (hMinusOneNorm h).toReal * √(gradNormSq (spaceGrad w))

The duality bound |∫ h w| ≤ ‖h‖_{HDot⁻¹} ‖∇w‖_{L²} for finite ‖h‖_{HDot⁻¹}.