Entrywise bounds for the defect matrices and ∇G

On the support of ξ_{m,k} (m ≥ 2, κ_m > 0), with e = ε_{m-1}^{2δ} and P = a_m ε_m²:

• |(D_k)_{ij}| ≤ 2 e P, |(E_k)_{ij}| ≤ 4 e P;
• |(G_{l_k})_j| ≤ 4 |∇T|;
• |(∇G_{l_k})_{ij}| ≤ 2 (h₀ + h₁) + 8 (2^16 ε_{m-1}⁻¹) |∇T|.

No oddness of k is needed: the flow estimates only use ξ_{m,k}(t) ≠ 0.

theorem AVenhance.Infra.Section5.Contracts.scf_e_le_one {β : ℝ} (I : Ingredients β) {m : ℕ} : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1

theorem AVenhance.Infra.Section5.Contracts.scf_e_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} : 0 ≤ epsilon β I.Λ (m - 1) ^ (2 * delta β)

theorem AVenhance.Infra.Section5.Contracts.scf_P_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} : 0 ≤ a β I.Λ m * epsilon β I.Λ m ^ 2

theorem AVenhance.Infra.Section5.Contracts.scf_grad_chi_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) (k : ℤ) (t : ℝ) (y : Homogenization.Vec 2) (u v : Fin 2) : |gradMatrix (fun (z : Homogenization.Vec 2) => I.chiMK κm m k t z) y u v| ≤ a β I.Λ m * epsilon β I.Λ m ^ 2 / κm

Entries of Χ_{m,k} gradient: |∂_aΧ_j| ≤ P/κ.

theorem AVenhance.Infra.Section5.Contracts.scf_sdDefect4_entry_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) {k : ℤ} {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (y : Homogenization.Vec 2) (i j : Fin 2) : |sdDefect4 I hΦ m κm k t y i j| ≤ 2 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (a β I.Λ m * epsilon β I.Λ m ^ 2)

theorem AVenhance.Infra.Section5.Contracts.scf_one_sub_transpose_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {k : ℤ} {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (y : Homogenization.Vec 2) (i a : Fin 2) : |(1 - (flowGradK I hΦ m k t y).transpose) i a| ≤ epsilon β I.Λ (m - 1) ^ (2 * delta β)

theorem AVenhance.Infra.Section5.Contracts.scf_sdDefect5_entry_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) {k : ℤ} {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (y : Homogenization.Vec 2) (i j : Fin 2) : |sdDefect5 I hΦ m κm k t y i j| ≤ 2 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2))

theorem AVenhance.Infra.Section5.Contracts.scf_G_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) {k : ℤ} (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) {gT : ℝ} (hg : ∀ (p : Fin 2), |spaceGrad (T t) x p| ≤ gT) (j : Fin 2) : |G I hΦ m T (lIdx β I.Λ m k) t x j| ≤ 2 * 2 * gT

theorem AVenhance.Infra.Section5.Contracts.scf_gradG_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) {k : ℤ} (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) {gT : ℝ} {h : Fin 2 → ℝ} (hg : ∀ (p : Fin 2), |spaceGrad (T t) x p| ≤ gT) (hh : ∀ (i p : Fin 2), |RelativeError.spaceHess (T t) x i p| ≤ h p) (i j : Fin 2) : |gradG I hΦ m T (lIdx β I.Λ m k) t x i j| ≤ 2 * (h 0 + h 1) + 8 * (2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹) * gT