Coordinate Cauchy estimates

These estimates reuse the one-variable Cauchy estimate on coordinate slices. The source has the supremum norm, so a coordinate disc fits in the ball of the same radius.

theorem CarlsonFunctions.SeveralComplexVariables.update_mem_closedBall {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {i : ι} {w : ℂ} {r : ℝ} (hr : 0 ≤ r) (hw : w ∈ Metric.closedBall (z i) r) : Function.update z i w ∈ Metric.closedBall z r

Updating one coordinate within its closed disc stays in the corresponding sup-norm ball.

theorem CarlsonFunctions.SeveralComplexVariables.norm_partialDeriv_le_of_slice {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : (ι → ℂ) → F} {z : ι → ℂ} (i : ι) {r M : ℝ} (hr : 0 < r) (hf : DifferentiableOn ℂ (fun (w : ℂ) => f (Function.update z i w)) (Metric.closedBall (z i) r)) (hM : ∀ w ∈ Metric.sphere (z i) r, ‖f (Function.update z i w)‖ ≤ M) : ‖partialDerivCarlson i f z‖ ≤ M / r

Cauchy's first derivative bound only needs holomorphy along the chosen coordinate disc.

theorem CarlsonFunctions.SeveralComplexVariables.norm_partialDeriv_le {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) {z : ι → ℂ} (i : ι) {r M : ℝ} (hr : 0 < r) (hball : Metric.closedBall z r ⊆ U) (hM : ∀ w ∈ Metric.closedBall z r, ‖f w‖ ≤ M) : ‖partialDerivCarlson i f z‖ ≤ M / r

A bound on a closed sup-norm ball controls every coordinate derivative at its center.