Skew integration by parts for the first coefficient derivative in the drift error.

theorem AVenhance.Infra.Section4.iterate_matrix_gradient_smooth {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (A x).mulVec (spaceGrad v x)

The actual matrix-gradient flux is smooth.

theorem AVenhance.Infra.Section4.iterate_matrix_gradient_periodic {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hv : ContDiff ℝ (↑⊤) v) (hA : IsZ2Periodic A) (hvp : IsZ2Periodic v) : IsZ2Periodic fun (x : Homogenization.Vec 2) => (A x).mulVec (spaceGrad v x)

Periodicity of the actual coefficient and scalar supplies flux periodicity.

theorem AVenhance.Infra.Section4.iterate_stream_pairing_transfer {ψ u v : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hψp : IsZ2Periodic ψ) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) : ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad u x) ((ψ x • sigmaMat).mulVec (spaceGrad v x)) = ∫ (x : Homogenization.Vec 2) in unitCube, u x * Homogenization.vecDot (sigmaMat.mulVec (spaceGrad ψ x)) (spaceGrad v x)

The first stream-coefficient derivative can be transferred to the coefficient once more, avoiding Young's inequality on the large first jet.

theorem AVenhance.Infra.Section4.iterate_scalar_transport_abs_bound {H a : ℝ} (hH : 0 < H) (b v : Homogenization.Vec 2) (hb : ∀ (j : Fin 2), |b j| ≤ H) : |a * Homogenization.vecDot b v| ≤ H * (a ^ 2 + Homogenization.vecNormSq v)

Pointwise bilinear bound after the skew transfer. The scalar norm is undifferentiated; both factors can then be controlled by lower-order energy.

theorem AVenhance.Infra.Section4.iterate_continuous_cell_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

Continuous cell integrands are integrable; this discharges the spatial integrability in the forcing estimates.

theorem AVenhance.Infra.Section4.iterateSpatialWord_sq_le_tail_gradient (f : Homogenization.Vec 2 → ℝ) (i : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateSpatialWord (i :: w) f x ^ 2 ≤ Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w f) x)

Any nonempty ordered scalar word is a component of a lower-order gradient.