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

The forward Jacobian is within B = 2^23 |t - s| a_{m-1} ≤ ε_{m-1}^{2δ}/4 of the identity in operator norm (section2_flow_close_from_previous), the inverse Jacobian entrywise (hence within 2B in operator norm); with ε_{m-1}^{2δ} ≤ 1/4 the sum is at most 3/16 ≤ 1/2.

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

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

theorem AVenhance.Infra.Section5.Contracts.sdn_flow_nearIdentity {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 4) {t : ℝ} {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}.