Strong material induction for spatial derivatives of transported scalars.

theorem AVenhance.Infra.Section4.amnr_material_gradient_mixed_abs_le_of_lower_gradient_bounds {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) {N cut : ℕ} {S H F Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hCb : 0 ≤ Cb) (z : AmnrSpace) (hfb : ∀ (η : List (Fin 2)) (r : ℕ), η.length + 2 * r ≤ N → |amnrWord b (amnrMixedWord η r) f z| ≤ F * S ^ η.length * H ^ r) (hBb : ∀ (p i : Fin 2) (η : List (Fin 2)), ∀ r < cut, η.length + 2 * r + 2 ≤ N → |amnrWord b (amnrMixedWord η r) (amnrVelocityGradient b p i) z| ≤ Cb * H * S ^ η.length * H ^ r) (n : ℕ) (hn : n ≤ cut) (α : List (Fin 2)) (j : ℕ) (hbudget : α.length + 1 + 2 * (n + j) ≤ N) (i : Fin 2) : |amnrWord b (amnrMixedWord α n) (amnrOp b (some i) (amnrWord b (List.replicate j none) f)) z| ≤ (1 + 2 ^ (N + 1) * Cb) ^ n * F * S ^ (α.length + 1) * H ^ (n + j)

A scalar's material/spatial jets control its differentiated material jets using only strictly lower material orders of the actual velocity gradient. This conditional calculus lemma does not assert the source primitive bounds.