Polydiscs and distinguished boundaries

Geometry for the polydisc Cauchy formula. Equal-radius polydiscs use the supremum norm; these are not Euclidean balls.

Closed polydiscs

def CarlsonFunctions.SeveralComplexVariables.closedPolydisc {ι : Type u_2} (c : ι → ℂ) (R : ℝ) : Set (ι → ℂ)

The closed polydisc of equal radii. For 0 ≤ R this coincides with the closed ball for the sup-norm.

Equations

• CarlsonFunctions.SeveralComplexVariables.closedPolydisc c R = Set.univ.pi fun (i : ι) => Metric.closedBall (c i) R

def CarlsonFunctions.SeveralComplexVariables.polydiscWithRadii {ι : Type u_2} (c : ι → ℂ) (r : ι → ℝ) : Set (ι → ℂ)

An open polydisc with a separate radius in each coordinate.

Equations

• CarlsonFunctions.SeveralComplexVariables.polydiscWithRadii c r = Set.univ.pi fun (i : ι) => Metric.ball (c i) (r i)

def CarlsonFunctions.SeveralComplexVariables.closedPolydiscWithRadii {ι : Type u_2} (c : ι → ℂ) (r : ι → ℝ) : Set (ι → ℂ)

A closed polydisc with a separate radius in each coordinate.

Equations

• CarlsonFunctions.SeveralComplexVariables.closedPolydiscWithRadii c r = Set.univ.pi fun (i : ι) => Metric.closedBall (c i) (r i)

@[simp]

theorem CarlsonFunctions.SeveralComplexVariables.mem_polydiscWithRadii {ι : Type u_2} {c z : ι → ℂ} {r : ι → ℝ} : z ∈ polydiscWithRadii c r ↔ ∀ (i : ι), dist (z i) (c i) < r i

Membership in a polydisc is a coordinatewise strict distance bound.

@[simp]

theorem CarlsonFunctions.SeveralComplexVariables.mem_closedPolydiscWithRadii {ι : Type u_2} {c z : ι → ℂ} {r : ι → ℝ} : z ∈ closedPolydiscWithRadii c r ↔ ∀ (i : ι), dist (z i) (c i) ≤ r i

Membership in a closed polydisc is a coordinatewise weak distance bound.

theorem CarlsonFunctions.SeveralComplexVariables.isOpen_polydiscWithRadii {ι : Type u_2} [Finite ι] (c : ι → ℂ) (r : ι → ℝ) : IsOpen (polydiscWithRadii c r)

A finite-dimensional polydisc is open.

theorem CarlsonFunctions.SeveralComplexVariables.isCompact_closedPolydiscWithRadii {ι : Type u_2} (c : ι → ℂ) (r : ι → ℝ) : IsCompact (closedPolydiscWithRadii c r)

A closed polydisc is compact, by the product compactness theorem.

theorem CarlsonFunctions.SeveralComplexVariables.closure_polydiscWithRadii {ι : Type u_2} (c : ι → ℂ) {r : ι → ℝ} (hr : ∀ (i : ι), 0 < r i) : closure (polydiscWithRadii c r) = closedPolydiscWithRadii c r

The closure of a positive-radius polydisc is the corresponding closed polydisc.

@[simp]

theorem CarlsonFunctions.SeveralComplexVariables.closedPolydiscWithRadii_const {ι : Type u_2} (c : ι → ℂ) (R : ℝ) : (closedPolydiscWithRadii c fun (x : ι) => R) = closedPolydisc c R

Equal coordinate radii recover the original closed-polydisc definition.

theorem CarlsonFunctions.SeveralComplexVariables.polydiscWithRadii_const_eq_ball {ι : Type u_2} [Fintype ι] (c : ι → ℂ) {R : ℝ} (hR : 0 < R) : (polydiscWithRadii c fun (x : ι) => R) = Metric.ball c R

In finite coordinates, equal positive radii give the open ball for the supremum norm.

theorem CarlsonFunctions.SeveralComplexVariables.polydiscWithRadii_mono {ι : Type u_2} (c : ι → ℂ) {r s : ι → ℝ} (hrs : ∀ (i : ι), r i ≤ s i) : polydiscWithRadii c r ⊆ polydiscWithRadii c s

Enlarging every radius enlarges the polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.closedPolydiscWithRadii_subset_polydiscWithRadii {ι : Type u_2} (c : ι → ℂ) {r s : ι → ℝ} (hrs : ∀ (i : ι), r i < s i) : closedPolydiscWithRadii c r ⊆ polydiscWithRadii c s

Strictly smaller closed coordinate discs lie in the larger open polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.continuous_torusMapWithRadii {n : ℕ} (c : Fin n → ℂ) (r : Fin n → ℝ) : Continuous (torusMap c r)

The torus parametrization with separate coordinate radii is continuous.

theorem CarlsonFunctions.SeveralComplexVariables.torusMap_coord_normWithRadii {n : ℕ} {c : Fin n → ℂ} {r : Fin n → ℝ} (hr : ∀ (i : Fin n), 0 ≤ r i) (θ : Fin n → ℝ) (i : Fin n) : ‖torusMap c r θ i - c i‖ = r i

Each torus coordinate has the prescribed nonnegative radius.

theorem CarlsonFunctions.SeveralComplexVariables.torusMap_mem_closedPolydiscWithRadii {n : ℕ} {c : Fin n → ℂ} {r : Fin n → ℝ} (hr : ∀ (i : Fin n), 0 ≤ r i) (θ : Fin n → ℝ) : torusMap c r θ ∈ closedPolydiscWithRadii c r

A torus with nonnegative radii belongs to its closed polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.cauchyKernel_ne_zero_on_torusWithRadii {n : ℕ} {c w : Fin n → ℂ} {r θ : Fin n → ℝ} {i : Fin n} (hr : ∀ (i : Fin n), 0 < r i) (hw : ‖w i - c i‖ < r i) : torusMap c r θ i ≠ w i

A Cauchy kernel has no pole on a coordinate circle when evaluated inside the polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.cons_mem_closedPolydiscWithRadii {n : ℕ} {c : Fin (n + 1) → ℂ} {r : Fin (n + 1) → ℝ} {x : ℂ} {y : Fin n → ℂ} (hx : x ∈ Metric.closedBall (c 0) (r 0)) (hy : y ∈ closedPolydiscWithRadii (c ∘ Fin.succ) (r ∘ Fin.succ)) : Fin.cons x y ∈ closedPolydiscWithRadii c r

Membership of a coordinate and the tail gives membership of the full polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.mem_closedPolydisc {n : ℕ} {c z : Fin n → ℂ} {R : ℝ} : z ∈ closedPolydisc c R ↔ ∀ (i : Fin n), z i ∈ Metric.closedBall (c i) R

Membership in an equal-radius closed polydisc is coordinatewise membership in the corresponding closed balls.

theorem CarlsonFunctions.SeveralComplexVariables.closedPolydisc_eq_closedBall {n : ℕ} {c : Fin n → ℂ} {R : ℝ} (hR : 0 ≤ R) : closedPolydisc c R = Metric.closedBall c R

An equal-radius closed polydisc is the closed ball for the supremum norm.

theorem CarlsonFunctions.SeveralComplexVariables.torusMap_mem_closedPolydisc {n : ℕ} {c : Fin n → ℂ} {R : ℝ} (hR : 0 ≤ R) (θ : Fin n → ℝ) : torusMap c (fun (x : Fin n) => R) θ ∈ closedPolydisc c R

The standard torus with nonnegative radius lies in its associated closed polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.cons_mem_closedPolydisc {n : ℕ} {c : Fin (n + 1) → ℂ} {R : ℝ} {x : ℂ} {y : Fin n → ℂ} (hx : x ∈ Metric.closedBall (c 0) R) (hy : y ∈ closedPolydisc (c ∘ Fin.succ) R) : Fin.cons x y ∈ closedPolydisc c R

Adjoining a point in the first coordinate ball to a point in the tail polydisc produces a point in the full polydisc.

theorem CarlsonFunctions.SeveralComplexVariables.continuous_torusMap {n : ℕ} (c : Fin n → ℂ) (R : ℝ) : Continuous (torusMap c fun (x : Fin n) => R)

The standard equal-radius torus parametrization is continuous.

theorem CarlsonFunctions.SeveralComplexVariables.two_pi_I_pow_ne_zero (n : ℕ) : (2 * ↑Real.pi * Complex.I) ^ n ≠ 0

No natural-number power of 2 * π * I vanishes.

theorem CarlsonFunctions.SeveralComplexVariables.torusMap_coord_norm {n : ℕ} {c : Fin n → ℂ} {R : ℝ} (hR : 0 ≤ R) (θ : Fin n → ℝ) (i : Fin n) : ‖torusMap c (fun (x : Fin n) => R) θ i - c i‖ = R

Every coordinate of the standard equal-radius torus has the prescribed distance from its center.

theorem CarlsonFunctions.SeveralComplexVariables.cauchyKernel_ne_zero_on_torus {n : ℕ} {c w : Fin n → ℂ} {R : ℝ} {θ : Fin n → ℝ} {i : Fin n} (hR : 0 < R) (hw : ‖w i - c i‖ < R) : torusMap c (fun (x : Fin n) => R) θ i ≠ w i

A point strictly inside a coordinate disc does not meet the corresponding coordinate circle, so its Cauchy kernel has no pole on the torus.