Second Frechet derivative bounds from one-variable Cauchy estimates. Symmetric bilinear polarization improves the mixed-coordinate constant when both sum and difference directions lie in the unit ball.

theorem KamProject.Arnold1963.deriv_line_eq_fderiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F} {x v : E} {z : ℂ} (hf : DifferentiableAt ℂ f (x + z • v)) : deriv (fun (w : ℂ) => f (x + w • v)) z = (fderiv ℂ f (x + z • v)) v

theorem KamProject.Arnold1963.iteratedDeriv_two_line_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : E → F} {U : Set E} {r : NNReal} {x v : E} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f U) (hx : x ∈ erosion U r) (hv : ‖v‖ ≤ 1) : iteratedDeriv 2 (fun (z : ℂ) => f (x + z • v)) 0 = ((fderiv ℂ (fderiv ℂ f) x) v) v

theorem KamProject.Arnold1963.norm_second_fderiv_diag_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {f : E → F} {U : Set E} {r : NNReal} {M : ℝ} {x v : E} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f U) (hM : NormBoundOn f U M) (hx : x ∈ erosion U r) (hv : ‖v‖ ≤ 1) : ‖((fderiv ℂ (fderiv ℂ f) x) v) v‖ ≤ 2 * M / ↑r ^ 2

theorem KamProject.Arnold1963.norm_second_fderiv_mixed_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : E → ℂ} {U : Set E} {r : NNReal} {M : ℝ} {x v w : E} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f U) (hM : NormBoundOn f U M) (hx : x ∈ erosion U r) (hplus : ‖v + w‖ ≤ 1) (hminus : ‖v - w‖ ≤ 1) : ‖((fderiv ℂ (fderiv ℂ f) x) v) w‖ ≤ M / ↑r ^ 2

theorem KamProject.Arnold1963.norm_second_coordinate_le {n : ℕ} {f : ComplexSpace n → ℂ} {U : Set (ComplexSpace n)} {r : NNReal} {M : ℝ} {x : ComplexSpace n} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f U) (hM : NormBoundOn f U M) (hx : x ∈ erosion U r) (i j : Fin n) : ‖((fderiv ℂ (fderiv ℂ f) x) (Pi.single i 1)) (Pi.single j 1)‖ ≤ 2 * M / ↑r ^ 2