Actual differentiated material-error energy for the previous increment.
theorem
AVenhance.Infra.Section4.iterate_material_error_gradient_sq_bound
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ))
{t : ℝ}
(ht : 0 < t)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
{B : ℝ}
(hB : ∀ (j k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => b t y k) x j| ≤ B)
:
Homogenization.vecNormSq
(spaceGrad
(fun (y : Homogenization.Vec 2) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) (t, y))
x) ≤ 2 * ∑ j : Fin 2,
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) (j :: w) (fun (z : AmnrSpace) => v z.1 z.2) (t, x) ^ 2 + 8 * B ^ 2 * Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (v t)) x)
Exact actual error-gradient expansion and the one-jet bound give its square in terms of longer error words and the undifferentiated gradient.
theorem
AVenhance.Infra.Section4.iterate_material_error_gradient_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))
{B : ℝ}
(hB :
∀ (t : ℝ) (x : Homogenization.Vec 2) (j k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => b t y k) x j| ≤ B)
:
(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad
(fun (y : Homogenization.Vec 2) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) (t, y))
x) ≤ (2 * ∑ j : Fin 2,
∫ (z : ℝ × Homogenization.Vec 2) in timeCube, iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) (j :: w) (fun (z : AmnrSpace) => v z.1 z.2) z ^ 2) + 8 * B ^ 2 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (v t))
The actual material-error gradient energy requires no differentiated error bound as a premise. All natural integrability is proved.