Analytic inputs of the centered ergodic estimates

The four statements below are assembled from the helper modules TermCenteredAnalytic{Window,Jets,Near,Smooth,Inputs,Compose}.

theorem AVenhance.Infra.Section5.Contracts.sd_flow_nearIdentity {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 4) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) {k : ℤ} (hξ : I.xiMK m k t ≠ 0) : Ergodic.FlowDerivativeNearIdentity (LeftToShow.xFlowDiffeo I hΦ m (lIdx β I.Λ m k) t)

Near-identity of the actual flow slice on the support of ξ_{m,k}.

theorem AVenhance.Infra.Section5.Contracts.sd_slow2_smooth_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (hTp : IsZ2Periodic (T t)) (k : ℤ) (a j : Fin 2) : ContDiff ℝ (↑⊤) (section5SlowChoice2 I hΦ m κm T k t a j) ∧ Ergodic.IsZPeriodic (section5SlowChoice2 I hΦ m κm T k t a j)

The two slow factors are smooth and ℤ²-periodic (any k).

theorem AVenhance.Infra.Section5.Contracts.sd_slow3_smooth_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (hTp : IsZ2Periodic (T t)) (k : ℤ) (a j : Fin 2) : ContDiff ℝ (↑⊤) (section5SlowChoice3 I hΦ m T k t a j) ∧ Ergodic.IsZPeriodic (section5SlowChoice3 I hΦ m T k t a j)