Actual forcing coefficient jets assembled from source primitive estimates.

theorem AVenhance.Infra.Section4.amnr_flowAverage_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (N : ℕ) (p j : Fin 2) : ContDiff ℝ (↑N) (amnrFlowAverage I hΦ m p j)

Smoothness of the actual flow average follows from local finiteness.

theorem AVenhance.Infra.Section4.amnr_temperatureCoefficient_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (κprev : ℝ) (i j : Fin 2) : ContDiff ℝ (↑(Nstar β)) (amnrTemperatureCoefficient I hΦ m κm κprev i j)

The actual coefficient has the finite joint regularity of Kmat.

theorem AVenhance.Infra.Section4.amnr_temperatureCoefficient_mixed_bound_of_components {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) (i j : Fin 2) {S T A B C D : ℝ} (hS : 0 ≤ S) (hT : 0 ≤ T) (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 0 ≤ D) (w : List (Option (Fin 2))) (hw : amnrBudget w ≤ Nstar β) (z : AmnrSpace) (hKbound : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (y : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) v (fun (y : AmnrSpace) => I.Kmat κm m y.1 i p) y| ≤ A * amnrWeight S T v) (hGbound : ∀ (p : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (y : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) v (amnrFlowAverage I hΦ m p j) y| ≤ B * amnrWeight S T v) (hPbound : ∀ (a b' : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (y : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) v (fun (y : AmnrSpace) => (I.Kmat κm m y.1 - κm • 1) a b') y| ≤ C * amnrWeight S T v) (hHbound : ∀ (a b' : Fin 2) (v : List (Option (Fin 2))), v.Sublist w → ∀ (y : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) v (fun (y : AmnrSpace) => amnrFlowAverageA0Plus I hΦ m a b' i j y - (if i = a then 1 else 0) * amnrFlowAverage I hΦ m b' j y) y| ≤ D * amnrWeight S T v) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (amnrTemperatureCoefficient I hΦ m κm κprev i j) z| ≤ (2 * 2 ^ Nstar β * A * B + |κprev * if i = j then 1 else 0| + 4 * 2 ^ Nstar β * C * D) * amnrWeight S T w

Mixed coefficient jets from the two actual left-Jacobian cutoff averages and the Kmat entries. The quadratic tensor is contracted row by row; its two flow factors are already represented by amnrFlowAverageA0Plus.