rectangle is convex hull

Stream: Is there code for X?

[Alex Kontorovich]

Is there an easy way to prove this? (Here $z$ and $w$ are two complex numbers, and I want to realize the axis-parallel rectangle with opposite corners z and w as the convex hull of those four points.) Thanks!

import Mathlib
open Complex Topology
set_option autoImplicit true
open scoped Interval

theorem rect_eq_convex_hull (z w : ℂ) :
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) =
      convexHull ℝ {z, w, z.re + w.im * I, w.re + z.im * I} := by
  sorry

[Yury G. Kudryashov]

You should prove a reProdIm version of convexHull_prod

[Yury G. Kudryashov]

Then you can write the set in the RHS as {z.re, w.re} ×ℂ {z.im, w.im}

[Yury G. Kudryashov]

Unfortunately, following equivalences is far from automatic.

[Yury G. Kudryashov]

I'll try to do it now

[Yury G. Kudryashov]

I have this:

import Mathlib.Analysis.Convex.Combination
import Mathlib.Data.Complex.Module

open scoped Interval

namespace Complex

lemma convexHull_reProdIm (s t : Set ℝ) :
    convexHull ℝ (s ×ℂ t) = convexHull ℝ s ×ℂ convexHull ℝ t :=
  calc
    convexHull ℝ (equivRealProdLm ⁻¹' (s ×ˢ t)) = equivRealProdLm ⁻¹' (convexHull ℝ (s ×ˢ t)) := by
      simpa only [← LinearEquiv.image_symm_eq_preimage]
        using equivRealProdLm.symm.toLinearMap.convexHull_image (s ×ˢ t)
    _ = convexHull ℝ s ×ℂ convexHull ℝ t := by rw [convexHull_prod]; rfl

lemma segment_reProdIm_segment_eq_convexHull (z w : ℂ) :
    [[z.re, w.re]] ×ℂ [[z.im, w.im]] = convexHull ℝ ({z.re, w.re} ×ℂ {z.im, w.im}) := by
  simp_rw [← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm]

end Complex

[Yury G. Kudryashov]

If you really want {z, w, z.re + w.im * I, w.re + z.im * I}, then you need to go along equivRealProd again.

[Yury G. Kudryashov]

This is a version with a different order of points:

import Mathlib.Analysis.Convex.Combination
import Mathlib.Data.Complex.Module

open Set
open scoped Interval

namespace Complex

lemma convexHull_reProdIm (s t : Set ℝ) :
    convexHull ℝ (s ×ℂ t) = convexHull ℝ s ×ℂ convexHull ℝ t :=
  calc
    convexHull ℝ (equivRealProdLm ⁻¹' (s ×ˢ t)) = equivRealProdLm ⁻¹' (convexHull ℝ (s ×ˢ t)) := by
      simpa only [← LinearEquiv.image_symm_eq_preimage]
        using equivRealProdLm.symm.toLinearMap.convexHull_image (s ×ˢ t)
    _ = convexHull ℝ s ×ℂ convexHull ℝ t := by rw [convexHull_prod]; rfl

lemma preimage_equivRealProd_prod (s t : Set ℝ) : equivRealProd ⁻¹' (s ×ˢ t) = s ×ℂ t := rfl

lemma segment_reProdIm_segment_eq_convexHull (z w : ℂ) :
    [[z.re, w.re]] ×ℂ [[z.im, w.im]] = convexHull ℝ {z, z.re + w.im * I, w.re + z.im * I, w} := by
  simp_rw [← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair,
    insert_union, ← insert_eq, Set.preimage_equiv_eq_image_symm, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]

end Complex

[Alex Kontorovich]

Great thanks! I'm trying to use this to see that a rectangle with all four endpoints in a disc is itself a subset of the disc. Do you see a better way to do this?

import Mathlib.Analysis.Convex.Combination
import Mathlib.Data.Complex.Module

open Set
open scoped Interval

namespace Complex

theorem rectangle_inside_disc {c : ℂ} {r : ℝ} {z w : ℂ} (hz : z ∈ Metric.ball c r)
    (hw : w ∈ Metric.ball c r)  (hzw : (z.re + w.im * I) ∈ Metric.ball c r)
    (hwz : (w.re + z.im * I) ∈ Metric.ball c r) :
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) ⊆ Metric.ball c r := by
  rw [rect_eq_convex_hull]
  convert convexHull_min ?_ (convex_ball c r)
  refine Set.insert_subset hz ?_
  refine Set.insert_subset hw ?_
  refine Set.insert_subset hzw ?_
  exact Set.singleton_subset_iff.mpr hwz

[Yury G. Kudryashov]

No, I don't have any better idea. If you generalize this lemma from Metric.ball to any convex set, then you can probably replace the last 4 lines with simp [*] (not tested)

[Yaël Dillies]

Also I am planning to formalise some material related to Krein-Milman, if ever you need to find the extreme points of a set (as the convex hull of those is your original set if it is convex, at least in finite dimensions).