Temporal product FTC at the actual initial boundary.
theorem
AVenhance.Infra.Section4.iterate_smooth_time_product_pairing
{u v : ℝ → Homogenization.Vec 2 → ℝ}
(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))
{T : ℝ}
(hT : 0 ≤ T)
(hI :
MeasureTheory.Integrable
(fun (p : AmnrSpace) =>
u p.1 p.2 * deriv (fun (s : ℝ) => v s p.2) 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)))
:
Product FTC for two actual smooth fields, with derivatives required only in the open time interval.
theorem
AVenhance.Infra.Section4.iterate_material_time_product_pairing
{φ u v : ℝ → Homogenization.Vec 2 → ℝ}
(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))
(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 : ℝ) => v s p.2) p.1)
((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)))
(hIvu :
MeasureTheory.Integrable (fun (p : AmnrSpace) => 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)))
:
∫ (t : ℝ) in 0..T, (∫ (x : Homogenization.Vec 2) in unitCube, u t x * amnrMaterial (streamVel φ) v t x) + ∫ (x : Homogenization.Vec 2) in unitCube, v t x * amnrMaterial (streamVel φ) u t x = (∫ (x : Homogenization.Vec 2) in unitCube, u T x * v T x) - ∫ (x : Homogenization.Vec 2) in unitCube, u 0 x * v 0 x
The spatial transport cancels in the actual product pairing, leaving only the endpoint product.