Exact stream-function divergence flux used in the differentiated energy equation.

theorem AVenhance.Infra.Section4.iterate_stream_matrix_smooth {φ : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => φ x • sigmaMat

The stream coefficient is spatially smooth whenever the actual stream is.

theorem AVenhance.Infra.Section4.iterate_stream_flux_divergence {φ u : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => (φ y • sigmaMat).mulVec (spaceGrad u y)) x = -Homogenization.vecDot (sigmaMat.mulVec (spaceGrad φ x)) (spaceGrad u x)

The sign of sigma gives divergence of φσ∇u equal to minus transport.

theorem AVenhance.Infra.Section4.iterateSpatialWord_neg (f : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) : iterateSpatialWord w (-f) = -iterateSpatialWord w f

Negation commutes with any spatial word.

theorem AVenhance.Infra.Section4.iterate_stream_word_flux_divergence {φ u : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hu : ContDiff ℝ (↑⊤) u) (w : List (Fin 2)) (x : Homogenization.Vec 2) : vecDiv (iterateWordFlux (fun (y : Homogenization.Vec 2) => φ y • sigmaMat) u w) x = -iterateSpatialWord w (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (sigmaMat.mulVec (spaceGrad φ y)) (spaceGrad u y)) x

The expanded stream flux is the negative differentiated transport.

theorem AVenhance.Infra.Section4.iterateWordMaterialError_stream_flux {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateWordMaterialError (fun (z : AmnrSpace) => streamVel φ z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x) = -vecDiv (iterateWordFlux (fun (y : Homogenization.Vec 2) => φ t y • sigmaMat) (u t) w) x + vecDiv (fun (y : Homogenization.Vec 2) => (φ t y • sigmaMat).mulVec (spaceGrad (iterateSpatialWord w (u t)) y)) x

Material commutators for the stream velocity are exactly the stream flux derivatives minus the principal skew flux.