Initial-time integrable representative of the actual commuted material gradient.
theorem
AVenhance.Infra.Section4.iterate_commuted_material_gradient_ae_representation
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F v : ℝ → Homogenization.Vec 2 → ℝ}
{v₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ F v₀ v)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
(fun (z : AmnrSpace) =>
spaceGrad (amnrMaterial b (fun (t : ℝ) => iterateSpatialWord w (v t)) z.1)
z.2) =ᵐ[MeasureTheory.volume.restrict timeCube]
fun (z : ℝ × Homogenization.Vec 2) =>
(κ • fun (j : Fin 2) =>
spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (v z.1)) y j) z.2) + spaceGrad (iterateSpatialWord w (F z.1)) z.2 - spaceGrad
(iterateVelocitySplit
(List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w)) (b z.1) (v z.1))
z.2
The actual PDE expresses the commuted material gradient through diffusion, original forcing, and the proved smooth representative of the drift error.
theorem
AVenhance.Infra.Section4.iterate_commuted_material_gradient_energy_integrable
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{F v : ℝ → Homogenization.Vec 2 → ℝ}
{v₀ : Homogenization.Vec 2 → ℝ}
(hsol : IsClassicalSol b κ F v₀ v)
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
(hFc : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (F z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ))
:
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) =>
Homogenization.vecNormSq (spaceGrad (amnrMaterial b (fun (t : ℝ) => iterateSpatialWord w (v t)) z.1) z.2))
timeCube MeasureTheory.volume
All natural material-gradient energy integrability follows from the actual equation and original forcing-jet continuity.