The homogeneous dual tests have zero mean, so the spectral estimate requires only the fast factor's mean. The high remainder is controlled in L2 by test Poincare, without a mean assumption on that remainder.

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_le_of_fastPeriodicProduct_without_product_mean {d N : ℕ} (hd : 0 < d) (hN : 0 < N) {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZPeriodic f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderiv : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(f x)) Cf r) {g : Homogenization.Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => |g x| ^ 2) MeasureTheory.volume) (hfast : IsFastPeriodic N g) (hNr : 2 ≤ r * ↑N) (hgMean : cellAverage g = 0) : (homogeneousHMinusOneNorm fun (x : Homogenization.Vec d) => f x * g x) ≤ ENNReal.ofReal ((1 + 64 * ergodicFourierWeight d ^ (1 / 2) + 1024 * (↑d + 1)) / ↑N * (cellAverage fun (x : Homogenization.Vec d) => |f x| ^ 2) ^ (1 / 2) * (cellAverage fun (x : Homogenization.Vec d) => |g x| ^ 2) ^ (1 / 2) + (1 + 64 * ergodicFourierWeight d ^ (1 / 2) + 1024 * (↑d + 1)) * Cf * (cellAverage fun (x : Homogenization.Vec d) => |g x| ^ 2) ^ (1 / 2) * Real.exp (-r * ↑N / 4096))