Ergodic estimates after a periodic volume-preserving flow

theorem AVenhance.Infra.Ergodic.FlowAverages.zPeriodic_comp_flow {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : IsZPeriodic f) (X : PeriodicVolumePreservingDiffeomorphism d) : IsZPeriodic fun (x : Homogenization.Vec d) => f (X.toFun x)

theorem AVenhance.Infra.Ergodic.FlowAverages.zPeriodic_square {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : IsZPeriodic f) : IsZPeriodic fun (x : Homogenization.Vec d) => f x ^ 2

theorem AVenhance.Infra.Ergodic.cellAverage_flow_mul_sub_le_of_composedCoordinateAnalyticL1Bounds {d N : ℕ} (hd : 0 < d) (hN : 0 < N) (X : PeriodicVolumePreservingDiffeomorphism d) {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZPeriodic f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderivComp : HasCoordinateAnalyticL1Bounds (fun (x : Homogenization.Vec d) => ↑(f (X.toFun x))) Cf r) {g : Homogenization.Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hfast : IsFastPeriodic N g) (hNr : 1 ≤ r * ↑N) : |(cellAverage fun (x : Homogenization.Vec d) => f x * g (X.invFun x)) - cellAverage f * cellAverage g| ≤ ((512 * Cf * cellAverage fun (x : Homogenization.Vec d) => |g x|) * ∑' (k : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖k‖)) * Real.exp (-(r * ↑N) / 1024)

Flow version of the basic L¹ covariance estimate. The derivative premise is placed on f ∘ X, which is the function to which the Fourier estimate is applied. Deriving it from averaged derivative bounds on f requires a separate quantitative composition theorem.