Iterates Centered Forcing Regularity #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_centered_hessian_forcing_joint_C1
{β : ℝ}
(I : Ingredients β)
(hN : 1 ≤ Nstar β)
{m : ℕ}
{κm : ℝ}
(hm : 1 ≤ m)
(hκm : 0 < κm)
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
The literal centered Hessian forcing has a joint C1 carrier. Only one time derivative of K is used, as available whenever the first iterate exists.
theorem
AVenhance.Infra.Section4.iterate_centered_hessian_forcing_gradient_continuousOn
{β : ℝ}
(I : Ingredients β)
(hN : 1 ≤ Nstar β)
{m : ℕ}
{κm : ℝ}
(hm : 1 ≤ m)
(hκm : 0 < κm)
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
ContinuousOn
(fun (z : AmnrSpace) =>
spaceGrad
(fun (y : Homogenization.Vec 2) =>
∑ j : Fin 2,
∑ k : Fin 2,
(I.Kmat κm m z.1 j k - timeAvgMat (I.Kmat κm m) j k) * iterateSpatialWord (j :: k :: w) (u z.1) y)
z.2)
(Set.Ici 0 ×ˢ Set.univ)
Natural joint continuity of the actual centered forcing gradient.