Documentation

Mathlib.Analysis.Complex.Convex

Theorems about convexity on the complex plane #

We show that the open and closed half-spaces in ℂ given by an inequality on either the real or imaginary part are all convex over ℝ. We also prove some results on star-convexity for the slit plane.

source
theorem Complex.convexHull_reProdIm (s t : Set ℝ) :
(convexHull ℝ) (s ×ℂ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t

A version of convexHull_prod for Set.reProdIm.

source
theorem Complex.starConvex_slitPlane {z : ℂ} (hz : 0 < z) :
StarConvex ℝ z Complex.slitPlane

The slit plane is star-convex at a positive number.

source
theorem Complex.starConvex_ofReal_slitPlane {x : ℝ} (hx : 0 < x) :
StarConvex ℝ (↑x) Complex.slitPlane

The slit plane is star-shaped at a positive real number.

source
theorem Complex.starConvex_one_slitPlane :
StarConvex ℝ 1 Complex.slitPlane

The slit plane is star-shaped at 1.

source
theorem convex_halfSpace_re_lt (r : ℝ) :
Convex ℝ {c : ℂ | c.re < r}
source
@[deprecated convex_halfSpace_re_lt (since := "2024-11-12")]
theorem convex_halfspace_re_lt (r : ℝ) :
Convex ℝ {c : ℂ | c.re < r}

Alias of convex_halfSpace_re_lt.

source
theorem convex_halfSpace_re_le (r : ℝ) :
Convex ℝ {c : ℂ | c.re ≤ r}
source
@[deprecated convex_halfSpace_re_le (since := "2024-11-12")]
theorem convex_halfspace_re_le (r : ℝ) :
Convex ℝ {c : ℂ | c.re ≤ r}

Alias of convex_halfSpace_re_le.

source
theorem convex_halfSpace_re_gt (r : ℝ) :
Convex ℝ {c : ℂ | r < c.re}
source
@[deprecated convex_halfSpace_re_gt (since := "2024-11-12")]
theorem convex_halfspace_re_gt (r : ℝ) :
Convex ℝ {c : ℂ | r < c.re}

Alias of convex_halfSpace_re_gt.

source
theorem convex_halfSpace_re_ge (r : ℝ) :
Convex ℝ {c : ℂ | r ≤ c.re}
source
@[deprecated convex_halfSpace_re_ge (since := "2024-11-12")]
theorem convex_halfspace_re_ge (r : ℝ) :
Convex ℝ {c : ℂ | r ≤ c.re}

Alias of convex_halfSpace_re_ge.

source
theorem convex_halfSpace_im_lt (r : ℝ) :
Convex ℝ {c : ℂ | c.im < r}
source
@[deprecated convex_halfSpace_im_lt (since := "2024-11-12")]
theorem convex_halfspace_im_lt (r : ℝ) :
Convex ℝ {c : ℂ | c.im < r}

Alias of convex_halfSpace_im_lt.

source
theorem convex_halfSpace_im_le (r : ℝ) :
Convex ℝ {c : ℂ | c.im ≤ r}
source
@[deprecated convex_halfSpace_im_le (since := "2024-11-12")]
theorem convex_halfspace_im_le (r : ℝ) :
Convex ℝ {c : ℂ | c.im ≤ r}

Alias of convex_halfSpace_im_le.

source
theorem convex_halfSpace_im_gt (r : ℝ) :
Convex ℝ {c : ℂ | r < c.im}
source
@[deprecated convex_halfSpace_im_gt (since := "2024-11-12")]
theorem convex_halfspace_im_gt (r : ℝ) :
Convex ℝ {c : ℂ | r < c.im}

Alias of convex_halfSpace_im_gt.

source
theorem convex_halfSpace_im_ge (r : ℝ) :
Convex ℝ {c : ℂ | r ≤ c.im}
source
@[deprecated convex_halfSpace_im_ge (since := "2024-11-12")]
theorem convex_halfspace_im_ge (r : ℝ) :
Convex ℝ {c : ℂ | r ≤ c.im}

Alias of convex_halfSpace_im_ge.

source
theorem Complex.isConnected_of_upperHalfPlane {r : ℝ} {s : Set ℂ} (hs₁ : {z : ℂ | r < z.im} ⊆ s) (hs₂ : s ⊆ {z : ℂ | r ≤ z.im}) :
IsConnected s
source
theorem Complex.isConnected_of_lowerHalfPlane {r : ℝ} {s : Set ℂ} (hs₁ : {z : ℂ | z.im < r} ⊆ s) (hs₂ : s ⊆ {z : ℂ | z.im ≤ r}) :
IsConnected s