Locally bounded separate holomorphy

Coordinate Cauchy estimates give joint local Lipschitz bounds for locally bounded, separately holomorphic functions. This supplies the continuity hypothesis of Osgood's theorem and the equicontinuity estimate used in Montel's theorem.

theorem CarlsonFunctions.SeveralComplexVariables.norm_sub_le_sum_of_update {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] {s : ι → Set ℂ} {f : (ι → ℂ) → F} {C : ℝ} (hf : ∀ z ∈ Set.univ.pi s, ∀ (i : ι), ∀ w ∈ s i, ‖f (Function.update z i w) - f z‖ ≤ C * ‖w - z i‖) {x y : ι → ℂ} (hx : x ∈ Set.univ.pi s) (hy : y ∈ Set.univ.pi s) : ‖f y - f x‖ ≤ ∑ i : ι, C * ‖y i - x i‖

Coordinate variation bounds telescope to a joint bound on a product set. This also includes the empty product, where every function is constant.

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

Updating a coordinate within its disc preserves a closed sup-norm ball.

theorem CarlsonFunctions.SeveralComplexVariables.norm_sub_le_of_separately_analytic_bounded {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {f : (ι → ℂ) → F} {c : ι → ℂ} {r M : ℝ} (hr : 0 < r) (hf : ∀ z ∈ Metric.closedBall c (2 * r), ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) (hM : ∀ z ∈ Metric.closedBall c (2 * r), ‖f z‖ ≤ M) {x y : ι → ℂ} (hx : x ∈ Metric.closedBall c r) (hy : y ∈ Metric.closedBall c r) : ‖f y - f x‖ ≤ ↑(Fintype.card ι) * (M / r) * ‖y - x‖

A bounded separately holomorphic map is jointly Lipschitz on a smaller polydisc. The constant is explicit and uniform over families with the same bound.

theorem CarlsonFunctions.SeveralComplexVariables.exists_lipschitzOnWith_of_separately_analytic_locally_bounded {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hU : IsOpen U) (hf : ∀ z ∈ U, ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) {c : ι → ℂ} (hc : c ∈ U) (hb : ∃ (M : ℝ), ∀ᶠ (z : ι → ℂ) in nhds c, ‖f z‖ ≤ M) : ∃ r > 0, ∃ (C : NNReal), LipschitzOnWith C f (Metric.closedBall c r)

Local bounds and separate holomorphy give a Lipschitz neighborhood of each point.

theorem CarlsonFunctions.SeveralComplexVariables.analyticOnNhd_of_separately_analytic_locally_bounded {ι : Type u_1} {F : Type u_2} [Fintype ι] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hU : IsOpen U) (hf : ∀ z ∈ U, ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) (hb : ∀ c ∈ U, ∃ (M : ℝ), ∀ᶠ (z : ι → ℂ) in nhds c, ‖f z‖ ≤ M) : AnalyticOnNhd ℂ f U

Locally bounded Osgood theorem. Joint continuity need not be assumed when a separately holomorphic map is locally bounded on its open domain.