Every primitive shear derivative with its exact physical amplitude and radius.

theorem AVenhance.Infra.Section4.amnr_iteratedFDeriv_comp_linear_norm_le {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : F → G} (hf : ContDiff ℝ (↑⊤) f) (L : E →L[ℝ] F) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (f ∘ ⇑L) x‖ ≤ ‖iteratedFDeriv ℝ n f (L x)‖ * ‖L‖ ^ n

Composition with a fixed linear operator has exactly its multilinear operator cost, without a factorial from the nonlinear chain rule.

theorem AVenhance.Infra.Section4.amnr_shear_iteratedFDeriv_norm_le {A L : ℝ} (hA : 0 ≤ A) (hL : 0 ≤ L) (i : Fin 2) (n : ℕ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => A * Real.sin (L * y i)) x‖ ≤ A * L ^ n

Every derivative of an actual sinusoidal shear is controlled by its frequency to that derivative order.

theorem AVenhance.Infra.Section4.amnr_psi_iteratedFDeriv_norm_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (n : ℕ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (psi β I.Λ m k) x‖ ≤ a β I.Λ m * epsilon β I.Λ m ^ 2 * (2 * Real.pi) ^ n * (epsilon β I.Λ m)⁻¹ ^ n

Every actual source profile has the physical stream amplitude a_m ε_m² and spatial radius ε_m, at every derivative order.