Appendix C composition in L1 and L2, retaining the same averaged norm. Only the L2 input includes order zero.

theorem AVenhance.Infra.Ergodic.spatialJet_eLpNorm_two_eq {d n : ℕ} {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (w : Fin n → Fin d) : MeasureTheory.eLpNorm (spatialJet n f w) 2 (MeasureTheory.volume.restrict (Torus.unitCell d)) = ENNReal.ofReal ((∫ (x : Homogenization.Vec d) in Torus.unitCell d, ‖spatialJet n f w x‖ ^ 2) ^ (1 / 2))

theorem AVenhance.Infra.Ergodic.hasCoordinateAnalyticL2Bounds_comp_of_mixed_bounds {d : ℕ} (hd : 0 < d) (X : PeriodicVolumePreservingDiffeomorphism d) {Cf r CX R : ℝ} (hCf : 0 ≤ Cf) (hr : 0 < r) (hCX : 0 < CX) (hR : 0 < R) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) (hfbound : ∀ (n : ℕ) (w : Fin n → Fin d), (∫ (x : Homogenization.Vec d) in Torus.unitCell d, ‖spatialJet n f w x‖ ^ 2) ^ (1 / 2) ≤ Cf * ↑n.factorial / r ^ n) (hXbound : ∀ (n : ℕ) (w : Fin n → Fin d), 0 < n → ∀ (x : Homogenization.Vec d) (j : Fin d), |spatialJet n X.toFun w x j| ≤ CX * ↑n.factorial * R ^ n) : HasCoordinateAnalyticL2Bounds (f ∘ X.toFun) Cf (r / (R * (r + ↑d * CX)))

Full mixed L2 input, including zero, gives the composed L2 predicate without any pointwise bound on the outer function.