Material integration by parts for the actual time primitive.
theorem
AVenhance.Infra.Section4.iterate_material_primitive_pairing
{φ u v : ℝ → Homogenization.Vec 2 → ℝ}
{q q' : ℝ → ℝ}
(hφ : IsAdmissibleStream φ)
(hu : ContDiffOn ℝ 1 (fun (p : AmnrSpace) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hv : ContDiffOn ℝ 1 (fun (p : AmnrSpace) => v p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hq : ContDiffOn ℝ 1 (fun (p : AmnrSpace) => q p.1) (Set.Ici 0 ×ˢ Set.univ))
(hdq : ∀ (t : ℝ), 0 < t → HasDerivAt q (q' t) t)
(hus : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (u t))
(hvs : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (v t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
{T : ℝ}
(hT : 0 ≤ T)
(hIuv :
MeasureTheory.Integrable (fun (p : AmnrSpace) => u p.1 p.2 * deriv (fun (s : ℝ) => q s * v s p.2) p.1)
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)))
(hIvu :
MeasureTheory.Integrable (fun (p : AmnrSpace) => q p.1 * v p.1 p.2 * deriv (fun (s : ℝ) => u s p.2) p.1)
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)))
(hJ :
MeasureTheory.Integrable (fun (p : AmnrSpace) => q' p.1 * u p.1 p.2 * v p.1 p.2)
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)))
(hU :
MeasureTheory.Integrable (fun (p : AmnrSpace) => q p.1 * u p.1 p.2 * amnrMaterial (streamVel φ) v p.1 p.2)
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)))
(hV :
MeasureTheory.Integrable (fun (p : AmnrSpace) => q p.1 * v p.1 p.2 * amnrMaterial (streamVel φ) u p.1 p.2)
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)))
:
∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, q' t * u t x * v t x = (((∫ (x : Homogenization.Vec 2) in unitCube, u T x * (q T * v T x)) - ∫ (x : Homogenization.Vec 2) in unitCube, u 0 x * (q 0 * v 0 x)) - ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, q t * u t x * amnrMaterial (streamVel φ) v t x) - ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, q t * v t x * amnrMaterial (streamVel φ) u t x
The primitive pairing retains the endpoint term and both material remainders. Derivatives at the initial boundary are never assumed.