Actual differentiated classical solutions, including the initial boundary.
theorem
AVenhance.Infra.Section4.iterate_classical_forcing_spatial_smooth
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ F u₀ u)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ))
{t : ℝ}
(ht : 0 < t)
:
Spatial smoothness of the actual forcing follows from the classical PDE and actual drift smoothness; it is not an extra forcing regularity premise.
theorem
AVenhance.Infra.Section4.iterate_classical_spatial_word_sol
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ F u₀ u)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
IsClassicalSol b κ
(fun (t : ℝ) (x : Homogenization.Vec 2) =>
iterateSpatialWord w (F t) x - iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x))
(iterateSpatialWord w u₀) fun (t : ℝ) => iterateSpatialWord w (u t)
Every spatial word of the actual scalar solves its actual differentiated PDE, with the explicit drift commutator subtracted from the forcing. Joint smoothness up to zero and the initial trace are proved from the original classical carrier. No differentiated classical equation is assumed.