Spatial skew transfer on every actual terminal-time cell.
theorem
AVenhance.Infra.Section4.IteratesTruncatedStream.truncated_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)
theorem
AVenhance.Infra.Section4.iterate_truncated_stream_pairing_transfer
{ψ 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))
{s : ℝ}
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
(hψp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (ψ t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
:
Skew transfer for actual smooth fields on timeCube, with all natural integrability discharged. The stream jet is differentiated once more.
theorem
AVenhance.Infra.Section4.iterate_truncated_stream_pairing_bound
{ψ u v : ℝ → Homogenization.Vec 2 → ℝ}
{H : ℝ}
(hH : 0 < H)
(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))
{s : ℝ}
(hs : 0 ≤ s)
(hs1 : s ≤ 1)
(hψp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (ψ t))
(hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t))
(hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t))
(hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2), |spaceGrad (ψ t) x j| ≤ H)
:
|∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2) ((ψ z.1 z.2 • sigmaMat).mulVec (spaceGrad (v z.1) z.2))| ≤ H * ((∫ (z : AmnrSpace) in iterateTruncatedCell s, u z.1 z.2 ^ 2) + ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecNormSq (spaceGrad (v z.1) z.2))
The transferred actual pairing uses scalar and gradient energies only; the large first stream derivative is absent from this bound.