Pointwise bounds for the twistie3, normie1, normie2 fluxes

At a fixed time t > 0 and point x, with μ = κ_m + a_m ε_m²:

• |D(t,x)_{ij}| ≤ μ for the diffusion matrix on the support of any odd ξ_{m,k};
• ∑_k ξ_{m,k} = 1, 0 ≤ ξ_{m,k} turn the k-uniform entry bound into a bound of the flux;
• twistie3: ∇T − G_{l_k} = −(∇X∘X⁻¹ − I)∇T (source e.monster.est.7);
• normie1: ΧTilde_k ∇G_{l_k} is the Hessian remainder of the leading-error work (source e.monster.est.10);
• normie2: D ∇HTilde_m (source e.monster.est.11).

The conclusions are squared-norm bounds |flux|² ≤ ∑_j c_j |V_j|² in the shape consumed by saTimeL2_le.

theorem AVenhance.Infra.Section5.Contracts.sa_vecNormSq_eq (v : Homogenization.Vec 2) : Homogenization.vecNormSq v = v 0 * v 0 + v 1 * v 1

theorem AVenhance.Infra.Section5.Contracts.sa_vecNormSq_le {v : Homogenization.Vec 2} {W : ℝ} (h : ∀ (i : Fin 2), |v i| ≤ W) : Homogenization.vecNormSq v ≤ 2 * W ^ 2

theorem AVenhance.Infra.Section5.Contracts.sa_sq3 (x y z : ℝ) : (x + y + z) ^ 2 ≤ 3 * (x ^ 2 + y ^ 2 + z ^ 2)

theorem AVenhance.Infra.Section5.Contracts.sa_sigma_abs_le (i j : Fin 2) : |sigmaMat i j| ≤ 1

theorem AVenhance.Infra.Section5.Contracts.sa_one_abs_le (i j : Fin 2) : |1 i j| ≤ 1

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

On the support of an odd ξ_{m,k} the diffusion matrix has entries at most κ_m + a_m ε_m².

theorem AVenhance.Infra.Section5.Contracts.sa_exists_xi_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∃ (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ≠ 0

A cutoff is nonzero for some odd index at every time.

theorem AVenhance.Infra.Section5.Contracts.sa_tsum_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (w : { k : ℤ // Odd k } → Homogenization.Vec 2) (W : ℝ) (hw : ∀ (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ≠ 0 → ∀ (i : Fin 2), |w k i| ≤ W) (i : Fin 2) : |(∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t • w k) i| ≤ W

Convex-combination bound.

twistie3

theorem AVenhance.Infra.Section5.Contracts.sa_gradT_sub_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) : |(spaceGrad (T t) x - G I hΦ m T (lIdx β I.Λ m k) t x) j| ≤ 2 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * gT

theorem AVenhance.Infra.Section5.Contracts.sa_twistie3Flux_vecNormSq_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) : Homogenization.vecNormSq (twistie3Flux I hΦ m κm T t x) ≤ (6 * ((κm + a β I.Λ m * epsilon β I.Λ m ^ 2) * epsilon β I.Λ (m - 1) ^ (2 * delta β))) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x)

normie2

theorem AVenhance.Infra.Section5.Contracts.sa_normie2Flux_vecNormSq_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.vecNormSq (normie2Flux I hΦ m κm T t x) ≤ (3 * (κm + a β I.Λ m * epsilon β I.Λ m ^ 2)) ^ 2 * Homogenization.vecNormSq (spaceGrad (fun (z : Homogenization.Vec 2) => I.Hm hΦ m κm T t z) x)

normie1

theorem AVenhance.Infra.Section5.Contracts.sa_chiGradG_eq_hessian {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (k : ℤ) (x : Homogenization.Vec 2) (i : Fin 2) : chiGradG I hΦ m κm T k t x i = RelativeError.leadingErrHessian I hΦ m κm T k t x i

ΧTilde_{m,k} ∇G_{l_k} is the Hessian remainder field of the leading-error work.

theorem AVenhance.Infra.Section5.Contracts.sa_chiGradG_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κ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 : Fin 2) : |chiGradG I hΦ m κm T k t x i| ≤ epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) * (4 * (h 0 + h 1) + 16 * (2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹) * gT)

theorem AVenhance.Infra.Section5.Contracts.sa_normie1Flux_vecNormSq_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) : Homogenization.vecNormSq (normie1Flux I hΦ m κm T t x) ≤ (40 * (2 * ((κm + a β I.Λ m * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm))) * (2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹))) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x) + (10 * (2 * ((κm + a β I.Λ m * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm))))) ^ 2 * Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [0] (T t)) x) + (10 * (2 * ((κm + a β I.Λ m * epsilon β I.Λ m ^ 2) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm))))) ^ 2 * Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [1] (T t)) x)