Actual homogeneous scalar material energy at every spatial order.
theorem
AVenhance.Infra.Section4.iterate_word_laplacian_continuousOn
{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) => spaceLap (iterateSpatialWord w (u z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ)
The scalar Laplacian of an actual word has a continuous initial-time carrier.
theorem
AVenhance.Infra.Section4.iterate_homogeneous_word_material_equation
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) u₀ u)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ))
{t : ℝ}
(ht : 0 < t)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
:
amnrMaterial b (fun (s : ℝ) => iterateSpatialWord w (u s)) t x = κ * spaceLap (iterateSpatialWord w (u t)) x - iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x)
The actual homogeneous PDE retains the complete drift commutator.
theorem
AVenhance.Infra.Section4.iterate_homogeneous_word_material_energy_bound
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{u : ℝ → Homogenization.Vec 2 → ℝ}
{u₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) u₀ u)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
∫ (z : ℝ × Homogenization.Vec 2) in timeCube, amnrMaterial b (fun (t : ℝ) => iterateSpatialWord w (u t)) z.1 z.2 ^ 2 ≤ (2 * κ ^ 2 * ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, spaceLap (iterateSpatialWord w (u z.1)) z.2 ^ 2) + 2 * ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) z ^ 2
Homogeneous material energy is derived from diffusion and the actual drift error. Its integrability follows from proved initial-time representatives.