All-order word bounds for the matrix entries Q, A, Y' of the slow factors

For t in the support of ξ_{m,k} the Section 2 bar-norm bounds (section2_flow_jacobian_composed_from_previous, section2_flow_inverse_regbounds_from_previous) bound all spatial derivatives of the entries of Q = ∇X ∘ X⁻¹ - I (constant 40, rate 2^10/ε) and of A = ∇X⁻¹ - I (constant 2^23 |t - s| a_{m-1}, rate 2^11/ε). They are converted to the ordered spatial word bounds of SlowFactorBoundsComposition.

Generic calculus

theorem AVenhance.Infra.Section5.Contracts.sdj_contDiff_gradMatrix_entry {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (a b : Fin 2) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => gradMatrix F y a b

theorem AVenhance.Infra.Section5.Contracts.sdj_word_sub_const (c : ℝ) (f : Homogenization.Vec 2 → ℝ) (i : Fin 2) (α : List (Fin 2)) : (Section4.amnrSpaceWord (i :: α) fun (y : Homogenization.Vec 2) => f y - c) = Section4.amnrSpaceWord (i :: α) f

theorem AVenhance.Infra.Section5.Contracts.sdj_word_le_of_barNorm {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) {R B : ℝ} (hR : 0 < R) (hB : 0 ≤ B) (hb : ∀ (n : ℕ), barNorm n R f ≤ ENNReal.ofReal B) (w : List (Fin 2)) (x : Homogenization.Vec 2) : |Section4.amnrSpaceWord w f x| ≤ B * ↑w.length.factorial * R ^ w.length

A bar-norm bound at every order gives the pointwise ordered word bound.

theorem AVenhance.Infra.Section5.Contracts.sdj_rate_mono {B R L : ℝ} (hB : 0 ≤ B) (hR : R ≤ L) (hR0 : 0 ≤ R) (n : ℕ) : B * ↑n.factorial * R ^ n ≤ B * ↑n.factorial * L ^ n

Jacobian entries

theorem AVenhance.Infra.Section5.Contracts.TermCenteredAnalyticJets.sdj_basisVec_norm_le_one (i : Fin 2) : ‖Homogenization.basisVec i‖ ≤ 1

theorem AVenhance.Infra.Section5.Contracts.TermCenteredAnalyticJets.sdj_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.Contracts.sdj_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.Contracts.sdj_contDiff_flowGrad_entry {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (a b : Fin 2) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => I.flowGrad hΦ m l t y a b

theorem AVenhance.Infra.Section5.Contracts.sdj_contDiff_invGrad_sub_one_entry {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (a b : Fin 2) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => (gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l t z) y - 1) a b

theorem AVenhance.Infra.Section5.Contracts.sdj_flowGrad_sub_one_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (y : Homogenization.Vec 2) (a b : Fin 2) : (I.flowGrad hΦ m l t y - 1) a b = (constructionComposedFlowJacobian hΦ (m - 1) (↑l * tauPP β I.Λ m) (t - ↑l * tauPP β I.Λ m) y - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) (Homogenization.basisVec a) b

The pulled forward Jacobian minus identity is the composed Section 2 Jacobian.

theorem AVenhance.Infra.Section5.Contracts.sdj_invGrad_sub_one_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (y : Homogenization.Vec 2) (a b : Fin 2) : (gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m l t z) y - 1) a b = (constructionFlowInvJacobian hΦ (m - 1) (t - ↑l * tauPP β I.Λ m) (↑l * tauPP β I.Λ m) y - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) (Homogenization.basisVec a) b

The inverse Jacobian minus identity is the Section 2 inverse Jacobian.

Bar-norm and word bounds

theorem AVenhance.Infra.Section5.Contracts.sdj_flowGrad_sub_one_barNorm {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (a b : Fin 2) (n : ℕ) : (barNorm n (2 ^ 10 * (epsilon β I.Λ (m - 1))⁻¹) fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m (lIdx β I.Λ m k) t y - 1) a b) ≤ ENNReal.ofReal 40

theorem AVenhance.Infra.Section5.Contracts.sdj_invGrad_sub_one_barNorm {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (a b : Fin 2) (n : ℕ) : (barNorm n (2 ^ 11 * (epsilon β I.Λ (m - 1))⁻¹) fun (y : Homogenization.Vec 2) => (gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m (lIdx β I.Λ m k) t z) y - 1) a b) ≤ ENNReal.ofReal (2 ^ 23 * |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| * AVenhance.a β I.Λ (m - 1))

theorem AVenhance.Infra.Section5.Contracts.sdj_eps_inv_pos {β : ℝ} (I : Ingredients β) (n : ℕ) : 0 < 2 ^ 10 * (epsilon β I.Λ n)⁻¹

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

All-order word bound for Q - 1 (the pulled forward Jacobian minus identity).

theorem AVenhance.Infra.Section5.Contracts.sdj_A_word_sharp {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (a b : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2) : |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => (gradMatrix (fun (z : Homogenization.Vec 2) => I.xFlowInv hΦ m (lIdx β I.Λ m k) t z) y - 1) a b) x| ≤ 2 ^ 23 * |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| * AVenhance.a β I.Λ (m - 1) * ↑w.length.factorial * (2 ^ 11 * (epsilon β I.Λ (m - 1))⁻¹) ^ w.length

All-order word bound for A = ∇X⁻¹ - I, with the sharp amplitude.

theorem AVenhance.Infra.Section5.Contracts.sdj_one_entry_abs_le (p q : Fin 2) : |1 p q| ≤ 1

theorem AVenhance.Infra.Section5.Contracts.sdj_rate_chain {β : ℝ} (I : Ingredients β) (n : ℕ) {L : ℝ} (hL : 2 ^ 11 * (epsilon β I.Λ n)⁻¹ ≤ L) : 2 ^ 10 * (epsilon β I.Λ n)⁻¹ ≤ L

theorem AVenhance.Infra.Section5.Contracts.sdj_Q_word {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) {L : ℝ} (hL : 2 ^ 11 * (epsilon β I.Λ (m - 1))⁻¹ ≤ L) (a b : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2) : |Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => I.flowGrad hΦ m (lIdx β I.Λ m k) t y a b) x| ≤ 41 * ↑w.length.factorial * L ^ w.length

All-order word bounds of the entries of Q = ∇X ∘ X⁻¹ (hQb of the composed lemma).