Actual squared material-error energy in analytic weights.
theorem
AVenhance.Infra.Section4.iterate_analytic_material_error_energy_bound
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
(a : ℕ)
{B G r L : ℝ}
(hL : 0 < L)
(hg : 2 * (r / L) ^ 2 ≤ 1 / 2)
(hjet :
∀ (t : ℝ) (x : Homogenization.Vec 2),
∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length)) (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)
(hE :
∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length)) (iterateSpatialSplits w),
(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ G ^ 2 * (↑(p.2.length + a).factorial * L ^ p.2.length) ^ 2)
:
Positive analytic velocity jets and actual lower scalar gradient energies control the material error square with one squared radius gain.