Natural integrability of the transported half-square cancellation.

theorem AVenhance.Infra.Section4.iterate_material_matrix_square_cancellation_of_smooth {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hQ : ∀ (i j : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => Q z.1 i j) (Set.Ici 0 ×ˢ Set.univ)) (hQd : ∀ (i j : Fin 2), Continuous fun (t : ℝ) => deriv (fun (s : ℝ) => Q s i j) t) (hH : ∀ (i j : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => H z.1 z.2 i j) (Set.Ici 0 ×ˢ Set.univ)) (hHs : ∀ (t : ℝ), 0 < t → ∀ (i j : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => H t x i j) (hHp : ∀ (t : ℝ), 0 < t → ∀ (i j : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => H t x i j) {s : ℝ} (hs : 0 ≤ s) : ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ i : Fin 2, ∑ j : Fin 2, deriv (fun (r : ℝ) => Q r i j) t * H t x i j) * ∑ i : Fin 2, ∑ j : Fin 2, Q t i j * H t x i j = ((l2NormSq fun (x : Homogenization.Vec 2) => ∑ i : Fin 2, ∑ j : Fin 2, Q s i j * H s x i j) - l2NormSq fun (x : Homogenization.Vec 2) => ∑ i : Fin 2, ∑ j : Fin 2, Q 0 i j * H 0 x i j) / 2 - ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ i : Fin 2, ∑ j : Fin 2, Q t i j * amnrMaterial (streamVel φ) (fun (r : ℝ) (y : Homogenization.Vec 2) => H r y i j) t x) * ∑ i : Fin 2, ∑ j : Fin 2, Q t i j * H t x i j

The half-square identity has no separately assumed temporal or material integrability. Continuous primitive derivatives and the actual C1 carriers supply every pairing, including the initial boundary.