The actual coarse material cancellation in the stream recursion.

theorem AVenhance.Infra.Section4.amnr_inverse_flow_material_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (s : ℝ) (z : AmnrSpace) : amnrOp (fun (y : AmnrSpace) => streamVel φ y.1 y.2) none (fun (y : AmnrSpace) => f (flowInv (streamVel φ) ⋯ ⋯ y.1 y.2 s)) z = 0

A scalar composed with the actual inverse flow is transported exactly. Both differentiability and the cancellation follow from the characterized flow.

theorem AVenhance.Infra.Section4.amnr_inverse_flow_material_product {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) {c : ℝ → ℝ} (hc : ContDiff ℝ 1 c) (s : ℝ) (z : AmnrSpace) : amnrOp (fun (y : AmnrSpace) => streamVel φ y.1 y.2) none (fun (y : AmnrSpace) => c y.1 * f (flowInv (streamVel φ) ⋯ ⋯ y.1 y.2 s)) z = deriv c z.1 * f (flowInv (streamVel φ) ⋯ ⋯ z.1 z.2 s)

Smooth time amplitudes times transported profiles have precisely the ordinary amplitude derivative as their coarse material derivative.

theorem AVenhance.Infra.Section4.amnr_inverse_flow_material_word {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) {c : ℝ → ℝ} {N : ℕ} (hc : ContDiff ℝ (↑N) c) (s : ℝ) (ℓ : ℕ) (hℓ : ℓ ≤ N) : (amnrWord (fun (y : AmnrSpace) => streamVel φ y.1 y.2) (List.replicate ℓ none) fun (y : AmnrSpace) => c y.1 * f (flowInv (streamVel φ) ⋯ ⋯ y.1 y.2 s)) = fun (y : AmnrSpace) => iteratedDeriv ℓ c y.1 * f (flowInv (streamVel φ) ⋯ ⋯ y.1 y.2 s)

Every pure material jet of a transported profile differentiates only its time amplitude. The inverse map is required only to be jointly C¹.

theorem AVenhance.Infra.Section4.amnr_psi_contDiff {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (psi β I.Λ m k)

The prescribed shear profile is smooth at every finite order.

theorem AVenhance.Infra.Section4.amnr_nextStreamTerm_material_word {β : ℝ} (I : Ingredients β) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (m : ℕ) (k : ℤ) (ℓ : ℕ) : (amnrWord (fun (y : AmnrSpace) => streamVel φ y.1 y.2) (List.replicate ℓ none) fun (y : AmnrSpace) => I.nextStreamTerm m φ hφ y.1 y.2 k) = fun (y : AmnrSpace) => iteratedDeriv ℓ (I.hatZetaML m (lIdx β I.Λ m k) * I.zetaMK m k) y.1 * psi β I.Λ m k (flowInv (streamVel φ) ⋯ ⋯ y.1 y.2 (↑(lIdx β I.Λ m k) * tauPP β I.Λ m))

Exact material jets of the actual stream-recursion summand. Coarse advection cancels the inverse-flow profile at every material order.