Spatial skew transfer on the full space-time cell.

theorem AVenhance.Infra.Section4.IteratesStreamSpaceTime.stream_pairing_continuous {ψ u v : ℝ → Homogenization.Vec 2 → ℝ} (hψ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => ψ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (z : AmnrSpace) => Homogenization.vecDot (spaceGrad (u z.1) z.2) ((ψ z.1 z.2 • sigmaMat).mulVec (spaceGrad (v z.1) z.2))) (Set.Ici 0 ×ˢ Set.univ) ∧ ContinuousOn (fun (z : AmnrSpace) => u z.1 z.2 * Homogenization.vecDot (sigmaMat.mulVec (spaceGrad (ψ z.1) z.2)) (spaceGrad (v z.1) z.2)) (Set.Ici 0 ×ˢ Set.univ)