normSq vs Metric.ball

Stream: Is there code for X?

[Alex Kontorovich]

This must already exist somewhere; any pointers please?

import Mathlib

theorem Complex.mem_ball_iff_normSq (c z : ℂ) (r : ℝ) (hr : 0 < r) : z ∈  Metric.ball c r ↔ normSq (z-c) < r^2 := by
  constructor
  · intro hz
    rw [mem_ball_iff_norm] at hz
    rw [Complex.normSq_eq_abs]
    rw [norm_eq_abs] at hz
    rw [sq_lt_sq]
    convert hz <;>  simp only [abs_abs, abs_eq_self]
    exact le_of_lt hr
  · intro hz
    refine mem_ball_iff_norm.mpr ?_
    rw [Complex.normSq_eq_abs] at hz
    rw [norm_eq_abs]
    nlinarith

[Eric Wieser]

You doubled the work for yourself by starting with constructor!

theorem Complex.mem_ball_iff_normSq (c z : ℂ) (r : ℝ) (hr : 0 ≤ r) :
    z ∈ Metric.ball c r ↔ normSq (z-c) < r^2 := by
  rw [mem_ball_iff_norm, normSq_eq_abs, norm_eq_abs, sq_lt_sq, abs_abs, abs_eq_self.mpr hr]

(edit: I relaxed hr)

[Eric Wieser]

That's basically the same lemmas you used, without writing each of them twice!

[Alex Kontorovich]

Ok but the theorem doesn't already exist, right? Should it?

[Yaël Dillies]

Well, why are you using normSq instead of ‖ ‖?

[Alex Kontorovich]

Hmm ok maybe I don't need it, if there's a slicker way to show that, for a complex rectangle whose corners are inside a ball, the whole rectangle is?...

import Mathlib

open Complex Topology

set_option autoImplicit true
open scoped Interval

theorem rectangle_inside_disc (c : ℂ) {r : ℝ} (hr : 0 < 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
  sorry

[Alex Kontorovich]

Is there something like: the rectangle is the convex hull of the four points; and the disc is convex. So the convex hull of points inside a convex set is itself inside the set??...

[Yury G. Kudryashov]

(continued in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/rectangle.20is.20convex.20hull )