Operator bounds extracted from actual source coordinate derivatives.

theorem AVenhance.Infra.Section4.amnr_multilinear_norm_le_two_pow_basis {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (L : Homogenization.Vec 2 [×n]→L[ℝ] F) {B : ℝ} (hB : 0 ≤ B) (h : ∀ (α : Fin n → Fin 2), ‖L fun (j : Fin n) => Homogenization.basisVec (α j)‖ ≤ B) : ‖L‖ ≤ 2 ^ n * B

On the actual Vec 2 carrier, an n-linear operator costs at most 2^n times the largest coordinate evaluation. The target may be any normed real space, including a higher derivative operator space.

theorem AVenhance.Infra.Section4.amnrSpaceWord_ofFn_eq_iteratedFDeriv {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (α : Fin n → Fin 2) : amnrSpaceWord (List.ofFn α) f = fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (α j)

Tuple-indexed spatial words give the actual iterated derivative without introducing a separate higher-derivative carrier.

theorem AVenhance.Infra.Section4.amnr_iteratedFDeriv_norm_le_of_spatial_words {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) {B : ℝ} (hB : 0 ≤ B) (hword : ∀ (α : List (Fin 2)), α.length = n → |amnrSpaceWord α f x| ≤ B) : ‖iteratedFDeriv ℝ n f x‖ ≤ 2 ^ n * B

Coordinate spatial-word bounds control the norm of the actual iterated Frechet derivative, uniformly over every derivative order.