Initial-time representatives of actual material matrix contractions.
theorem
AVenhance.Infra.Section4.iterate_material_matrix_contraction_square_integrable
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
{H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hQ : ∀ (j k : Fin 2), ContinuousOn (fun (t : ℝ) => Q t j k) (Set.Ici 0))
(hH : ∀ (j k : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => H z.1 z.2 j k) (Set.Ici 0 ×ˢ Set.univ))
:
MeasureTheory.IntegrableOn
(fun (z : AmnrSpace) =>
(∑ j : Fin 2,
∑ k : Fin 2, Q z.1 j k * amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => H t x j k) z.1 z.2) ^ 2)
timeCube MeasureTheory.volume
A time-only continuous matrix and actual C1 scalar entries give an integrable square of the material contraction, including the initial boundary.
theorem
AVenhance.Infra.Section4.iterate_material_matrix_contraction_energy_bound
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
{H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(hQc : ∀ (j k : Fin 2), ContinuousOn (fun (t : ℝ) => Q t j k) (Set.Ici 0))
(hH : ∀ (j k : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => H z.1 z.2 j k) (Set.Ici 0 ×ˢ Set.univ))
{D G : ℝ}
(hD : 0 ≤ D)
(hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ D)
(hE :
∀ (j k : Fin 2),
∫ (z : ℝ × Homogenization.Vec 2) in timeCube, amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => H t x j k) z.1 z.2 ^ 2 ≤ G ^ 2)
:
Actual entrywise material energies control the actual primitive contraction. Natural integrability is proved from the C1 carriers, not separately assumed.