The energy inequality with the actual spatial drift commutator retained.

theorem AVenhance.Infra.Section4.TemperatureForcedEnergy.amnr_cell_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section4.TemperatureForcedEnergy.amnr_normSq_continuous {a : Homogenization.Vec 2 → Homogenization.Vec 2} (ha : Continuous a) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecNormSq (a x)