From the actual Amnr spatial word calculus to the Appendix C predicates.

theorem AVenhance.Infra.Section5.slowFactor_word_ofFn_eq_spatialJet {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (w : Fin n → Fin 2) : Section4.amnrSpaceWord (List.ofFn w) f = Ergodic.spatialJet n f w

theorem AVenhance.Infra.Section5.slowFactor_spatialJet_realCast {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (w : Fin n → Fin 2) (x : Homogenization.Vec 2) : Ergodic.spatialJet n (fun (y : Homogenization.Vec 2) => ↑(f y)) w x = ↑(Ergodic.spatialJet n f w x)

theorem AVenhance.Infra.Section5.slowFactor_hasCoordinateAnalyticL2Bounds_comp (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : Ergodic.IsZPeriodic f) {F L CX R : ℝ} (hF : 0 ≤ F) (hL : 0 < L) (hCX : 0 < CX) (hR : 0 < R) (hb : ∀ (w : List (Fin 2)), MeasureTheory.eLpNorm (Section4.amnrSpaceWord w f) 2 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (F * ↑w.length.factorial * L ^ w.length)) (hX : ∀ (n : ℕ) (w : Fin n → Fin 2), 0 < n → ∀ (x : Homogenization.Vec 2) (j : Fin 2), |Ergodic.spatialJet n X.toFun w x j| ≤ CX * ↑n.factorial * R ^ n) : Ergodic.HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec 2) => ↑(f (X.toFun x))) F (L⁻¹ / (R * (L⁻¹ + 2 * CX)))

Full mixed bounds, rather than the weaker pure-coordinate predicate, feed the sharp averaged composition theorem.