Actual full forcing coefficient jets at every spatial order.
theorem
AVenhance.Infra.Section4.iterateMatrixWord_constant_add
{A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hA : ContDiff ℝ (↑⊤) A)
(B : Matrix (Fin 2) (Fin 2) ℝ)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
:
iterateMatrixWord (fun (y : Homogenization.Vec 2) => B + A y) w x = (if w = [] then B else 0) + iterateMatrixWord A w x
A time-only coefficient contributes only at spatial order zero.
theorem
AVenhance.Infra.Section4.iterate_TForcing_coefficient_word_continuousOn
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
(κprev : ℝ)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(w : List (Fin 2))
:
ContinuousOn
(fun (z : AmnrSpace) =>
iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m z.1 - κprev • 1 + I.sMat hΦ m κm z.1 y) w z.2)
(Set.Ici 0 ×ˢ Set.univ)
Every jet of the actual full TForcing coefficient is jointly continuous up to zero, as a consequence of the conditional flow carrier.