Centered Spectral Flow

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_le_of_fastPeriodicProduct_flow_without_product_mean {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 : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(f (X.toFun 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) (hnear : FlowDerivativeNearIdentity X) (hgMean : cellAverage g = 0) : (homogeneousHMinusOneNorm fun (x : Homogenization.Vec d) => f x * g (X.invFun x)) ≤ ENNReal.ofReal (3 * ↑d ^ 2 * ((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)))