Quantitative actual differentiated material commutator after transfer.
theorem
AVenhance.Infra.Section4.iterate_terminal_transferred_material_error_analytic_bound
{s : ℝ}
(hs1 : s ≤ 1)
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{u v : ℝ → Homogenization.Vec 2 → ℝ}
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hQc : ContinuousOn Q (Set.Ici 0))
(hbp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (b t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
(w : List (Fin 2))
(i : ℕ)
{Qmax B Gprev Gcur r L : ℝ}
(hQmax : 0 ≤ Qmax)
(hB : 0 ≤ B)
(hGp : 0 ≤ Gprev)
(hGc : 0 ≤ Gcur)
(hr : 0 ≤ r)
(hL : 0 < L)
(hgain : r / L ≤ 1 / 2)
(D : ℕ → ℝ)
(hD : ∀ (n : ℕ), 0 ≤ D n)
(hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ Qmax)
(hjet :
∀ (t : ℝ) (x : Homogenization.Vec 2),
∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w),
∀ (j : Fin 2),
|iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ B * ↑p.1.length.factorial * r ^ p.1.length)
(hprev :
∀ (k : Fin 2),
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord (k :: w) (v t))) ≤ (Gprev * ↑(w.length + 2 * i - 1).factorial * L ^ (w.length + 1)) ^ 2)
(hcur :
∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w),
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (u t))) ≤ (Gcur * ↑(p.2.length + 2 * i).factorial * L ^ p.2.length * D p.2.length) ^ 2)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot
(spaceGrad
(fun (y : Homogenization.Vec 2) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (z.1, y))
z.2)
((Q z.1).mulVec (spaceGrad (iterateSpatialWord w (v z.1)) z.2))| ≤ 8 * Qmax * B * Gprev * Gcur * r * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * ∑ k ∈ Finset.range w.length, (1 / 2) ^ k * D (w.length - 1 - k)
The actual gradient commutator has the linear geometric recurrence bound after spatial transfer, with no extra current scalar derivative.