Integrable representatives of actual material errors and their gradients.
theorem
AVenhance.Infra.Section4.iterate_material_error_ae_lower_velocity
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
(fun (z : AmnrSpace) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2)
z) =ᵐ[MeasureTheory.volume.restrict timeCube]
fun (z : ℝ × Homogenization.Vec 2) =>
iterateVelocitySplit (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w))
(b z.1) (v z.1) z.2
On the positive cell the actual material error is the explicit lower velocity sum, whose initial-time smooth representative is proved.
theorem
AVenhance.Infra.Section4.iterate_material_error_gradient_ae_lower_velocity
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
(fun (z : AmnrSpace) =>
spaceGrad
(fun (y : Homogenization.Vec 2) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) (z.1, y))
z.2) =ᵐ[MeasureTheory.volume.restrict timeCube]
fun (z : ℝ × Homogenization.Vec 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 spatial gradient equals the gradient of the lower velocity representative almost everywhere on timeCube.
theorem
AVenhance.Infra.Section4.iterate_material_error_energy_integrable
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) z ^ 2)
timeCube MeasureTheory.volume
The actual scalar material-error square is integrable.
theorem
AVenhance.Infra.Section4.iterate_material_error_gradient_energy_integrable
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{v : ℝ → Homogenization.Vec 2 → ℝ}
(hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) =>
Homogenization.vecNormSq
(spaceGrad
(fun (y : Homogenization.Vec 2) =>
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) (z.1, y))
z.2))
timeCube MeasureTheory.volume
The actual material-error gradient square is integrable.