Flow facts on supp ξ_{m,k} for the twistie1 source contract

Everything is stated for the flow slice X_{m-1,l_k}(t) at a time where ξ_{m,k}(t) ≠ 0:

• the time window |t - l_k τ''_m| ≤ 2^{-25} a_{m-1}^{-1} (se_window);
• the all-order derivative bound of the flow slice (se_xFlow_jet_le, e.Xm.bound.4);
• the all-order jets of the flow gradient (se_flowGrad_word_le, window form of iterate_flowGrad_word_bound, which assumes ξ̂_{m,l}(t) ≠ 0 instead);
• the near-identity condition of the App C flow lemma (se_nearIdentity).

theorem AVenhance.Infra.Section5.Contracts.se_window {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹

The source time window on the support of ξ_{m,k}.

theorem AVenhance.Infra.Section5.Contracts.se_xFlow_jet_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (n : ℕ) (hn : 1 ≤ n) (J : Fin n → Fin 2) (x : Homogenization.Vec 2) : ‖(iteratedFDeriv ℝ n (I.xFlow hΦ m (lIdx β I.Λ m k) t) x) fun (j : Fin n) => Homogenization.basisVec (J j)‖ ≤ 2 * ↑n.factorial * (2 ^ 14 * (epsilon β I.Λ (m - 1))⁻¹) ^ (n - 1)

All-order derivative bound of the flow slice on the support of ξ_{m,k} (e.Xm.bound.4, coordinate form).

theorem AVenhance.Infra.Section5.Contracts.se_flowGrad_barNorm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {l : ℤ} {t : ℝ} (hwin : |t - ↑l * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹) (n : ℕ) (i j : Fin 2) : (barNorm n (2 ^ 10 * (epsilon β I.Λ (m - 1))⁻¹) fun (x : Homogenization.Vec 2) => (I.flowGrad hΦ m l t x - 1) i j) ≤ ENNReal.ofReal 40

Window form of iterate_flowGrad_barNorm.

theorem AVenhance.Infra.Section5.Contracts.se_flowGrad_word_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {l : ℤ} {t : ℝ} (hwin : |t - ↑l * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : |Section4.iterateSpatialWord w (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) i j) x| ≤ 40 * ↑w.length.factorial * (2 ^ 10 / epsilon β I.Λ (m - 1)) ^ w.length

Window form of iterate_flowGrad_word_bound: the jets of ∇X ∘ X⁻¹ - 1.

theorem AVenhance.Infra.Section5.Contracts.se_amnrSpaceWord_add_const (f : Homogenization.Vec 2 → ℝ) (c : ℝ) (w : List (Fin 2)) : w ≠ [] → (Section4.amnrSpaceWord w fun (y : Homogenization.Vec 2) => f y + c) = Section4.amnrSpaceWord w f

Adding a constant does not change a nonempty ordered derivative word.

theorem AVenhance.Infra.Section5.Contracts.se_flowGrad_entry_jet_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1) {L : ℝ} (hL : 2 ^ 10 / epsilon β I.Λ (m - 1) ≤ L) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => I.flowGrad hΦ m (lIdx β I.Λ m k) t y i j) x| ≤ 40 * ↑w.length.factorial * L ^ w.length

Jets of the entries of the flow gradient itself (order zero: |∇X ∘ X⁻¹| ≤ 2).

theorem AVenhance.Infra.Section5.Contracts.se_opNorm_le_of_entries (A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) {b : ℝ} (hb : 0 ≤ b) (h : ∀ (i j : Fin 2), |A (Homogenization.basisVec i) j| ≤ b) : ‖A‖ ≤ 2 * b

The operator norm of a map on Vec 2 (sup norm) is at most twice the largest matrix entry.

theorem AVenhance.Infra.Section5.Contracts.se_gradMatrix_apply {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Differentiable ℝ F) (x : Homogenization.Vec 2) (i j : Fin 2) : gradMatrix F x i j = (fderiv ℝ F x) (Homogenization.basisVec i) j

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

Near-identity of the flow slice on the support of ξ_{m,k} (the hypothesis of the App C flow lemma): ε_{m-1}^{2δ} ≤ 1/8 gives ‖∇X - I‖ + ‖∇X⁻¹ - I‖ ≤ 1/2.