Mean-value estimates on contained segments. Coordinate bounds give operator bounds with the explicit dimension factor required by the maximum norm.

theorem KamProject.Arnold1963.norm_sub_le_of_segment_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {U : Set E} {a b : E} {C : ℝ} (hab : segment ℝ a b ⊆ U) (hf : ∀ x ∈ U, DifferentiableAt ℂ f x) (hC : NormBoundOn (fderiv ℂ f) U C) : ‖f b - f a‖ ≤ C * ‖b - a‖

theorem KamProject.Arnold1963.norm_sub_le_of_analytic_segment_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {U : Set E} {a b : E} {C : ℝ} (hab : segment ℝ a b ⊆ U) (hf : AnalyticOnNhd ℂ f U) (hC : NormBoundOn (fderiv ℂ f) U C) : ‖f b - f a‖ ≤ C * ‖b - a‖

theorem KamProject.Arnold1963.norm_linearMap_le_of_coordinate_bound {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (A : ComplexSpace n →L[ℂ] F) {C : ℝ} (hC : 0 ≤ C) (hA : ∀ (j : Fin n), ‖A (Pi.single j 1)‖ ≤ C) : ‖A‖ ≤ ↑n * C

theorem KamProject.Arnold1963.norm_sub_le_of_coordinate_bound {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ComplexSpace n → F} {U : Set (ComplexSpace n)} {a b : ComplexSpace n} {C : ℝ} (hab : segment ℝ a b ⊆ U) (hf : AnalyticOnNhd ℂ f U) (hC : 0 ≤ C) (hbound : ∀ x ∈ U, ∀ (j : Fin n), ‖(fderiv ℂ f x) (Pi.single j 1)‖ ≤ C) : ‖f b - f a‖ ≤ ↑n * C * ‖b - a‖