Polydiscs centred at real points

A ball in ι → ℂ for the sup norm is a polydisc: each coordinate of a point of ball 0 r has modulus less than r. When its centre is a real point fun i ↦ (a i : ℂ), taking real parts maps it into the ball of the same radius around a in ι → ℝ, and it is invariant under complex conjugation.

Main declarations

• Complex.pi_norm_div_lt_one_of_mem_ball: every coordinate of a point of the polydisc ball 0 r has modulus less than r, so dividing it by r lands in the unit disc.
• Complex.pi_re_mem_ball: the real part of a point of the polydisc lies in the real ball.
• Complex.pi_ofReal_re_mem_ball: the real part, viewed as a complex point, lies in the polydisc.
• Complex.pi_star_mem_ball_iff: the polydisc is invariant under complex conjugation.
• Complex.pi_star_mem_iUnion_ball_iff: a union of such polydiscs is invariant under complex conjugation.
• Complex.pi_ofReal_mem_iUnion_ball_iff: the real points of a union of polydiscs centred at the points of U ⊆ ι → ℝ, whose real points lie in U, are exactly the points of U.

theorem Complex.pi_norm_div_lt_one_of_mem_ball {ι : Type u_1} [Fintype ι] {r : ℝ} {z : ι → ℂ} (hz : z ∈ Metric.ball 0 r) (i : ι) : ‖z i / ↑r‖ < 1

Every coordinate of a point of the polydisc ball 0 r, divided by r, lies in the unit disc.

theorem Complex.pi_re_mem_ball {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {r : ℝ} {z : ι → ℂ} (hz : z ∈ Metric.ball (fun (i : ι) => ↑(a i)) r) : (fun (i : ι) => (z i).re) ∈ Metric.ball a r

The real part of a point of a polydisc centred at a real point a lies in the ball of the same radius around a.

theorem Complex.pi_ofReal_re_mem_ball {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {r : ℝ} {z : ι → ℂ} (hz : z ∈ Metric.ball (fun (i : ι) => ↑(a i)) r) : (fun (i : ι) => ↑(z i).re) ∈ Metric.ball (fun (i : ι) => ↑(a i)) r

The real part of a point of a polydisc centred at a real point, viewed as a complex point, lies in the polydisc.

theorem Complex.pi_star_mem_ball_iff {ι : Type u_1} [Fintype ι] {a : ι → ℝ} {r : ℝ} {z : ι → ℂ} : star z ∈ Metric.ball (fun (i : ι) => ↑(a i)) r ↔ z ∈ Metric.ball (fun (i : ι) => ↑(a i)) r

A polydisc centred at a real point is invariant under complex conjugation.

theorem Complex.pi_star_mem_iUnion_ball_iff {ι : Type u_1} [Fintype ι] {z : ι → ℂ} {α : Sort u_2} {c : α → ι → ℝ} {s : α → ℝ} : star z ∈ ⋃ (x : α), Metric.ball (fun (i : ι) => ↑(c x i)) (s x) ↔ z ∈ ⋃ (x : α), Metric.ball (fun (i : ι) => ↑(c x i)) (s x)

A union of polydiscs centred at real points is invariant under complex conjugation.

theorem Complex.pi_ofReal_mem_iUnion_ball_iff {ι : Type u_1} [Fintype ι] {U : Set (ι → ℝ)} {s : ↑U → ℝ} (hs : ∀ (x : ↑U), 0 < s x) (hsU : ∀ (x : ↑U), Metric.ball (↑x) (s x) ⊆ U) {y : ι → ℝ} : (fun (i : ι) => ↑(y i)) ∈ ⋃ (x : ↑U), Metric.ball (fun (i : ι) => ↑(↑x i)) (s x) ↔ y ∈ U

The real points of a union of polydiscs of positive radii centred at the points of U, whose real points lie in U, are exactly the points of U.