Pointwise bounds for the tiny source contract

Pure pointwise (in (t, x)) calculus for the last-iterate error e_{m-1}:

• e = -B ∇V where V = T_{N*} - T_{N*-1} is the last increment and B = K_m - κ_{m-1} I + s_{m-1};
• the Leibniz expansion of ∇(∇ · (B ∇V)) into the words of length ≤ 2 applied to V, with the coefficient jets of B (sc_gradDiv_abs_le);
• the pointwise bound of the nondivergence part ∑_k ξ_{m,k} χTilde_{m,k} · (∇X ∘ X⁻¹) ∇(∇ · e) by |∇(∇ · e)| (sc_nd_sq_le).

Only products of coordinate bounds are used; the constants are crude since the source (7900–7925) leaves an enormous amount of room (N_* large).

def AVenhance.Infra.Section5.Contracts.scWords2 : Finset (List (Fin 2))

The seven words of length at most two.

Equations

• AVenhance.Infra.Section5.Contracts.scWords2 = {[], [0], [1], [0, 0], [0, 1], [1, 0], [1, 1]}

theorem AVenhance.Infra.Section5.Contracts.mem_scWords2 {w : List (Fin 2)} (hw : w.length ≤ 2) : w ∈ scWords2

theorem AVenhance.Infra.Section5.Contracts.sc_gradDiv_flux_eq {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x i = ∑ k : Fin 2, Section4.iterateWordFlux A v [k, i] x k

|∇ ∇·(A ∇v)| in terms of ordered Leibniz splits of the words [k, i].

theorem AVenhance.Infra.Section5.Contracts.sc_list_abs_sum_le {α : Type u_1} (L : List α) (f : α → ℝ) (c : ℝ) (h : ∀ a ∈ L, |f a| ≤ c) : |(List.map f L).sum| ≤ ↑L.length * c

theorem AVenhance.Infra.Section5.Contracts.sc_flux_term_abs_le {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (x : Homogenization.Vec 2) {D r : ℝ} (hD : 0 ≤ D) (hr : 1 ≤ r) (hAj : ∀ (p : List (Fin 2)), p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord A p x j k| ≤ D * ↑p.length.factorial * r ^ p.length) (w : List (Fin 2)) (hw : w.length = 2) {p : List (Fin 2) × List (Fin 2)} (hp : p ∈ Section4.iterateSpatialSplits w) (k j : Fin 2) : |Section4.iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A y k j) x * spaceGrad (Section4.iterateSpatialWord p.2 v) x j| ≤ 2 * D * r ^ 2 * ∑ w' ∈ scWords2, √(Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord w' v) x))

Each term of the expanded flux of ∇ ∇·(A ∇v) is bounded by the coefficient jets times the gradient of a word of length ≤ 2 applied to v.

theorem AVenhance.Infra.Section5.Contracts.sc_gradDiv_abs_le {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (x : Homogenization.Vec 2) {D r : ℝ} (hD : 0 ≤ D) (hr : 1 ≤ r) (hAj : ∀ (p : List (Fin 2)), p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord A p x j k| ≤ D * ↑p.length.factorial * r ^ p.length) (i : Fin 2) : |spaceGrad (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x i| ≤ 32 * D * r ^ 2 * ∑ w ∈ scWords2, √(Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord w v) x))

Pointwise bound of ∇ ∇·(A ∇v) by the coefficient jets of A (orders ≤ 2) and the gradients of the words of length ≤ 2 applied to v.

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

theorem AVenhance.Infra.Section5.Contracts.sc_card_scWords2 : scWords2.card = 7

theorem AVenhance.Infra.Section5.Contracts.sc_gradDiv_vecNormSq_le {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (x : Homogenization.Vec 2) {D r : ℝ} (hD : 0 ≤ D) (hr : 1 ≤ r) (hAj : ∀ (p : List (Fin 2)), p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord A p x j k| ≤ D * ↑p.length.factorial * r ^ p.length) : Homogenization.vecNormSq (spaceGrad (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x) ≤ 14336 * D ^ 2 * r ^ 4 * ∑ w ∈ scWords2, Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord w v) x)

|∇ ∇·(A ∇v)|² is bounded by the sum of the squares of the word gradients.

theorem AVenhance.Infra.Section5.Contracts.sc_mulVec_vecNormSq_le {M : Matrix (Fin 2) (Fin 2) ℝ} {b : ℝ} (g : Homogenization.Vec 2) (hM : ∀ (i j : Fin 2), |M i j| ≤ b) : Homogenization.vecNormSq (M.mulVec g) ≤ 4 * b ^ 2 * Homogenization.vecNormSq g

A matrix with entries of size ≤ b maps g to a vector of squared norm ≤ 4 b² |g|².

theorem AVenhance.Infra.Section5.Contracts.sc_xi_support_finset {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : ∃ (s : Finset ℤ), s.card ≤ 3 ∧ ∀ (k : ℤ), I.xiMK m k t ≠ 0 → k ∈ s

A window of width 5/2 around t/τ_m contains at most three integers k, so at most three ξ_{m,k}(t) are nonzero.

theorem AVenhance.Infra.Section5.Contracts.sc_xiMK_abs_le_one {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (t : ℝ) : |I.xiMK m k t| ≤ 1

theorem AVenhance.Infra.Section5.Contracts.sc_nd_sq_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) {cχ : ℝ} (hχ : ∀ (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2), |I.chiTilde hΦ m κm k t x j| ≤ cχ) (x : Homogenization.Vec 2) : tinyNondivergencePart I hΦ m κm e t x ^ 2 ≤ 5184 * cχ ^ 2 * Homogenization.vecNormSq (gradDiv e t x)

Pointwise bound of the nondivergence part of tiny by |∇(∇·e)|.

theorem AVenhance.Infra.Section5.Contracts.sc_spaceGrad_neg (f : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => -f y) x = -spaceGrad f x

theorem AVenhance.Infra.Section5.Contracts.sc_vecDiv_neg (H : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => -H y) x = -vecDiv H x

noncomputable def AVenhance.Infra.Section5.Contracts.scCoeff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev t : ℝ) (y : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The coefficient matrix of the last-iterate error.

Equations

• AVenhance.Infra.Section5.Contracts.scCoeff I hΦ m κm κprev t y = I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y

theorem AVenhance.Infra.Section5.Contracts.sc_iterateError_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hN : 1 ≤ Nstar β) (hTa : ContDiff ℝ (↑⊤) (T (Nstar β) t)) (hTb : ContDiff ℝ (↑⊤) (T (Nstar β - 1) t)) (y : Homogenization.Vec 2) : iterateError I hΦ m κm κprev T t y = -(scCoeff I hΦ m κm κprev t y).mulVec (spaceGrad (Section4.iterateIncrement T (Nstar β) t) y)

e_{m-1} = -B ∇V for the last increment V = T_{N*} - T_{N*-1}.

theorem AVenhance.Infra.Section5.Contracts.sc_vecNormSq_neg (v : Homogenization.Vec 2) : Homogenization.vecNormSq (-v) = Homogenization.vecNormSq v

theorem AVenhance.Infra.Section5.Contracts.sc_e_vecNormSq_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hN : 1 ≤ Nstar β) (hTa : ContDiff ℝ (↑⊤) (T (Nstar β) t)) (hTb : ContDiff ℝ (↑⊤) (T (Nstar β - 1) t)) (x : Homogenization.Vec 2) {b : ℝ} (hb : ∀ (j k : Fin 2), |scCoeff I hΦ m κm κprev t x j k| ≤ b) : Homogenization.vecNormSq (iterateError I hΦ m κm κprev T t x) ≤ 4 * b ^ 2 * Homogenization.vecNormSq (spaceGrad (Section4.iterateIncrement T (Nstar β) t) x)

Pointwise L² bound of e_{m-1} by the gradient of the last increment.

theorem AVenhance.Infra.Section5.Contracts.sc_gradDiv_error_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hN : 1 ≤ Nstar β) (hTa : ContDiff ℝ (↑⊤) (T (Nstar β) t)) (hTb : ContDiff ℝ (↑⊤) (T (Nstar β - 1) t)) (x : Homogenization.Vec 2) : gradDiv (iterateError I hΦ m κm κprev T) t x = -spaceGrad (vecDiv fun (y : Homogenization.Vec 2) => (scCoeff I hΦ m κm κprev t y).mulVec (spaceGrad (Section4.iterateIncrement T (Nstar β) t) y)) x

∇(∇·e) is minus the gradient of the divergence of the flux B ∇V.

theorem AVenhance.Infra.Section5.Contracts.sc_nd_sq_le_words {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm κprev : ℝ} (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hN : 1 ≤ Nstar β) (hTa : ContDiff ℝ (↑⊤) (T (Nstar β) t)) (hTb : ContDiff ℝ (↑⊤) (T (Nstar β - 1) t)) (hAs : ContDiff ℝ (↑⊤) (scCoeff I hΦ m κm κprev t)) {cχ : ℝ} (hχ : ∀ (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2), |I.chiTilde hΦ m κm k t x j| ≤ cχ) (x : Homogenization.Vec 2) {D r : ℝ} (hD : 0 ≤ D) (hr : 1 ≤ r) (hAj : ∀ (p : List (Fin 2)), p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord (scCoeff I hΦ m κm κprev t) p x j k| ≤ D * ↑p.length.factorial * r ^ p.length) : tinyNondivergencePart I hΦ m κm (iterateError I hΦ m κm κprev T) t x ^ 2 ≤ 5184 * cχ ^ 2 * (14336 * D ^ 2 * r ^ 4) * ∑ w ∈ scWords2, Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord w (Section4.iterateIncrement T (Nstar β) t)) x)

Pointwise bound of the nondivergence part of tiny by the word gradients of the last increment, from the coefficient jets of B of orders ≤ 2.