Ordered spatial words connect to the stream-regularity barNorm carrier.

theorem AVenhance.Infra.Section4.iterateSpatialWord_eq_iteratedFDeriv {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) : iterateSpatialWord w f = fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ w.length f x) fun (j : Fin w.length) => Homogenization.basisVec (w.get j)

Ordered words are the coordinate evaluations of the Frechet jets.

theorem AVenhance.Infra.Section4.iterate_continuous_enorm_le_eLpNorm_top {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (x : Homogenization.Vec 2) : ‖f x‖ₑ ≤ MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume

Continuity turns a volume essential-supremum bound into a pointwise bound.

theorem AVenhance.Infra.Section4.iterate_word_enorm_bound_of_barNorm {f : Homogenization.Vec 2 → ℝ} {R B : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hR : 0 < R) (w : List (Fin 2)) (hbar : barNorm w.length R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖iterateSpatialWord w f x‖ₑ ≤ ENNReal.ofReal B / (ENNReal.ofReal ((↑w.length + 1) ^ 2 / ↑w.length.factorial) * (ENNReal.ofReal R)⁻¹ ^ w.length)

Literal barNorm bounds supply every actual ordered spatial jet pointwise. The ENNReal normalization is retained exactly as in the definition.

theorem AVenhance.Infra.Section4.iterate_word_abs_bound_of_barNorm {f : Homogenization.Vec 2 → ℝ} {R B : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hR : 0 < R) (hB : 0 ≤ B) (w : List (Fin 2)) (hbar : barNorm w.length R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : |iterateSpatialWord w f x| ≤ B / ((↑w.length + 1) ^ 2 / ↑w.length.factorial * R⁻¹ ^ w.length)

Real form of the barNorm jet bound, with its exact analytic normalization.

theorem AVenhance.Infra.Section4.iterate_word_abs_factorial_bound_of_barNorm {f : Homogenization.Vec 2 → ℝ} {R B : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hR : 0 < R) (hB : 0 ≤ B) (w : List (Fin 2)) (hbar : barNorm w.length R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : |iterateSpatialWord w f x| ≤ B * ↑w.length.factorial * R ^ w.length / (↑w.length + 1) ^ 2

The real analytic normalization is a factorial times the radius power.