Flow near-identity on supp ξ_{m,k} (e.Xm.bound.1, e.Xm.bound.2)

For t in the support of ξ_{m,k} the flow time t - l_k τ''_m is at most τ''_m, which is at most 2^{-25} ε_{m-1}^{2-β+2δ}. The Section 2 flow bounds at level m - 1 therefore give ‖∇X⁻¹ - I‖, ‖∇X - I‖ ≤ 2^{23} |t - l_k τ''_m| a_{m-1} ≤ ε_{m-1}^{2δ} / 4, entrywise, together with the second-derivative bound 2^16 ε_{m-1}⁻¹ for the flow slice.

All statements are unconditional: only IsStreamSeq I Φ is assumed.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.eps_pos {β : ℝ} (I : Ingredients β) (n : ℕ) : 0 < epsilon β I.Λ n

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.xiMK_ne_zero_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) {k : ℤ} {t : ℝ} (hne : I.xiMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 5 / 4 * tau β I.Λ m

theorem AVenhance.Infra.Section5.RelativeError.xi_flow_time_window_tauPP {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ tauPP β I.Λ m

Refined window: on supp ξ_{m,k}, |t - l_k τ''_m| ≤ τ''_m.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.scale_arith {e b x d : ℝ} (he : 0 < e) (hx : x ≤ 2 ^ (-25) * e ^ (2 - b + 2 * d)) : 2 ^ 23 * x * e ^ (b - 2) ≤ e ^ (2 * d) / 4

Abstract-real scale arithmetic: if x ≤ 2^{-25} e^{2-b+2δ} then 2^23 x e^{b-2} ≤ e^{2δ}/4.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.scale_window {e b x d : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hd : 0 ≤ d) (hx : x ≤ 2 ^ (-25) * e ^ (2 - b + 2 * d)) : x ≤ 2 ^ (-25) * (e ^ (b - 2))⁻¹

Abstract-real scale arithmetic: 2^{-25} e^{2-b+2δ} ≤ 2^{-25} (e^{b-2})⁻¹ for e ≤ 1, 0 ≤ δ.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.flow_window_scale {β : ℝ} (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))⁻¹ ∧ 2 ^ 23 * |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| * a β I.Λ (m - 1) ≤ epsilon β I.Λ (m - 1) ^ (2 * delta β) / 4

Flow-time window and the resulting smallness 2^23 |t - l_kτ''| a_{m-1} ≤ ε_{m-1}^{2δ}/4.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.basisVec_norm_le_one (i : Fin 2) : ‖Homogenization.basisVec i‖ ≤ 1

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.clm_entry_le (A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (i j : Fin 2) : |A (Homogenization.basisVec i) j| ≤ ‖A‖

Entry bound for a continuous linear map on Vec 2.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.fderiv_coord {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Differentiable ℝ F) (x : Homogenization.Vec 2) (j : Fin 2) (v : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => F y j) x) v = (fderiv ℝ F x) v j

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.gradMatrix_sub_one_apply {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Differentiable ℝ F) (x : Homogenization.Vec 2) (i j : Fin 2) : (gradMatrix F x - 1) i j = (fderiv ℝ F x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) (Homogenization.basisVec i) j

gradMatrix minus identity as a Jacobian entry.

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.xFlow_slice_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : (fun (y : Homogenization.Vec 2) => I.xFlow hΦ m l t y) = fun (y : Homogenization.Vec 2) => constructionFlow hΦ (m - 1) (↑l * tauPP β I.Λ m + (t - ↑l * tauPP β I.Λ m)) y (↑l * tauPP β I.Λ m)

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.xFlowInv_slice_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y) = fun (y : Homogenization.Vec 2) => constructionFlowInv hΦ (m - 1) (↑l * tauPP β I.Λ m + (t - ↑l * tauPP β I.Λ m)) y (↑l * tauPP β I.Λ m)

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.xFlow_diff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : Differentiable ℝ fun (y : Homogenization.Vec 2) => I.xFlow hΦ m l t y

theorem AVenhance.Infra.Section5.RelativeError.LeadingErrorFlow.xFlowInv_diff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : Differentiable ℝ fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y

theorem AVenhance.Infra.Section5.RelativeError.gradMatrix_xFlowInv_sub_one_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) (i j : Fin 2) : |(gradMatrix (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m (lIdx β I.Λ m k) t y) x - 1) i j| ≤ epsilon β I.Λ (m - 1) ^ (2 * delta β)

e.Xm.bound.1 for the inverse flow, entrywise, on supp ξ_{m,k}.

theorem AVenhance.Infra.Section5.RelativeError.flowGrad_sub_one_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) (i j : Fin 2) : |(I.flowGrad hΦ m (lIdx β I.Λ m k) t x - 1) i j| ≤ epsilon β I.Λ (m - 1) ^ (2 * delta β)

e.Xm.bound.1 for the forward flow pulled back (the flowGrad), entrywise.

theorem AVenhance.Infra.Section5.RelativeError.xFlow_second_deriv_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) (i j l : Fin 2) : |(iteratedFDeriv ℝ 2 (fun (y : Homogenization.Vec 2) => I.xFlow hΦ m (lIdx β I.Λ m k) t y l) x) ![Homogenization.basisVec i, Homogenization.basisVec j]| ≤ 2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹

Second spatial derivatives of the flow slice (e.Xm.bound.2 / e.flow.for.ergodic, n = 2).