The sup metric and axis-parallel squares

The blueprint takes the Euclidean norm as primary and uses the sup norm for the axis-parallel objects the polygonal work is built on: grids of small squares, the vertex squares of the redrawing argument, and the large square a bounded set is caught inside. Appendix C item 1 asks for the comparison ‖x‖∞ ≤ ‖x‖ ≤ √2 ‖x‖∞, which is supNorm_le_norm and norm_le_sqrt_two_mul_supNorm here.

The one theorem of substance is isConnected_beyondSquare: the plane outside a closed square is connected. It is a square and not a disk on purpose — the outside of a square is exactly a union of four half-planes, each convex, with consecutive ones sharing a point, whereas the outside of a disk would need the polar decomposition this development withholds.

Blueprint

• supNorm, supDist — Appendix C, item 1 (the sup metric).
• supNorm_le_norm, norm_le_sqrt_two_mul_supNorm — the comparison, used without comment.
• closedSquare, openSquare — the axis-parallel square about a point.
• isConnected_beyondSquare — the outside of a square is connected; what makes exactly one face of a plane graph unbounded.

Coordinates

theorem Schoenflies.Plane.sub_apply (x y : Plane) (i : Fin 2) : (x - y).ofLp i = x.ofLp i - y.ofLp i

theorem Schoenflies.Plane.smul_add_apply (a b : ℝ) (x y : Plane) (i : Fin 2) : (a • x + b • y).ofLp i = a * x.ofLp i + b * y.ofLp i

theorem Schoenflies.Plane.continuous_coord (i : Fin 2) : Continuous fun (x : Plane) => x.ofLp i

The sup norm

noncomputable def Schoenflies.Plane.supNorm (x : Plane) : ℝ

The sup norm ‖x‖∞ = max |x₁| |x₂|.

Equations

• x.supNorm = max |x.ofLp 0| |x.ofLp 1|

noncomputable def Schoenflies.Plane.supDist (x y : Plane) : ℝ

The sup distance.

Equations

• x.supDist y = (x - y).supNorm

theorem Schoenflies.Plane.supNorm_nonneg (x : Plane) : 0 ≤ x.supNorm

theorem Schoenflies.Plane.supDist_nonneg (x y : Plane) : 0 ≤ x.supDist y

@[simp]

theorem Schoenflies.Plane.supDist_self (x : Plane) : x.supDist x = 0

theorem Schoenflies.Plane.supDist_comm (x y : Plane) : x.supDist y = y.supDist x

theorem Schoenflies.Plane.abs_sub_zero_le_supDist (x y : Plane) : |x.ofLp 0 - y.ofLp 0| ≤ x.supDist y

theorem Schoenflies.Plane.abs_sub_one_le_supDist (x y : Plane) : |x.ofLp 1 - y.ofLp 1| ≤ x.supDist y

theorem Schoenflies.Plane.abs_zero_le_supNorm (x : Plane) : |x.ofLp 0| ≤ x.supNorm

theorem Schoenflies.Plane.abs_one_le_supNorm (x : Plane) : |x.ofLp 1| ≤ x.supNorm

theorem Schoenflies.Plane.supDist_triangle (x y z : Plane) : x.supDist z ≤ x.supDist y + y.supDist z

The sup distance satisfies the triangle inequality, one coordinate at a time.

theorem Schoenflies.Plane.norm_sq_eq (x : Plane) : ‖x‖ ^ 2 = x.ofLp 0 ^ 2 + x.ofLp 1 ^ 2

theorem Schoenflies.Plane.supNorm_le_norm (x : Plane) : x.supNorm ≤ ‖x‖

Half of Appendix C item 1's comparison: the sup norm is at most the Euclidean norm.

theorem Schoenflies.Plane.norm_le_sqrt_two_mul_supNorm (x : Plane) : ‖x‖ ≤ √2 * x.supNorm

The other half: the Euclidean norm is at most √2 times the sup norm.

Coordinate half-planes

One convexity proof per direction serves all four sides of a square, and the outside of a square is four of them.

theorem Schoenflies.Plane.convex_coord_le (i : Fin 2) (r : ℝ) : Convex ℝ {x : Plane | x.ofLp i ≤ r}

theorem Schoenflies.Plane.convex_coord_ge (i : Fin 2) (r : ℝ) : Convex ℝ {x : Plane | r ≤ x.ofLp i}

theorem Schoenflies.Plane.convex_coord_lt (i : Fin 2) (r : ℝ) : Convex ℝ {x : Plane | x.ofLp i < r}

theorem Schoenflies.Plane.convex_coord_gt (i : Fin 2) (r : ℝ) : Convex ℝ {x : Plane | r < x.ofLp i}

theorem Schoenflies.Plane.isOpen_coord_lt (i : Fin 2) (r : ℝ) : IsOpen {x : Plane | x.ofLp i < r}

theorem Schoenflies.Plane.isOpen_coord_gt (i : Fin 2) (r : ℝ) : IsOpen {x : Plane | r < x.ofLp i}

Axis-parallel squares

def Schoenflies.Plane.closedSquare (c : Plane) (r : ℝ) : Set Plane

The closed axis-parallel square of radius r about c.

Equations

• c.closedSquare r = {x : Schoenflies.Plane | x.supDist c ≤ r}

def Schoenflies.Plane.openSquare (c : Plane) (r : ℝ) : Set Plane

The open axis-parallel square of radius r about c.

Equations

• c.openSquare r = {x : Schoenflies.Plane | x.supDist c < r}

theorem Schoenflies.Plane.closedSquare_eq_inter (c : Plane) (r : ℝ) : c.closedSquare r = {x : Plane | c.ofLp 0 - r ≤ x.ofLp 0} ∩ {x : Plane | x.ofLp 0 ≤ c.ofLp 0 + r} ∩ ({x : Plane | c.ofLp 1 - r ≤ x.ofLp 1} ∩ {x : Plane | x.ofLp 1 ≤ c.ofLp 1 + r})

theorem Schoenflies.Plane.openSquare_eq_inter (c : Plane) (r : ℝ) : c.openSquare r = {x : Plane | c.ofLp 0 - r < x.ofLp 0} ∩ {x : Plane | x.ofLp 0 < c.ofLp 0 + r} ∩ ({x : Plane | c.ofLp 1 - r < x.ofLp 1} ∩ {x : Plane | x.ofLp 1 < c.ofLp 1 + r})

theorem Schoenflies.Plane.convex_closedSquare (c : Plane) (r : ℝ) : Convex ℝ (c.closedSquare r)

theorem Schoenflies.Plane.convex_openSquare (c : Plane) (r : ℝ) : Convex ℝ (c.openSquare r)

theorem Schoenflies.Plane.isOpen_openSquare (c : Plane) (r : ℝ) : IsOpen (c.openSquare r)

theorem Schoenflies.Plane.isClosed_closedSquare (c : Plane) (r : ℝ) : IsClosed (c.closedSquare r)

The outside of a square

def Schoenflies.Plane.beyondSquare (r : ℝ) : Set Plane

The plane outside the closed square of radius r about the origin.

Equations

• Schoenflies.Plane.beyondSquare r = {x : Schoenflies.Plane | r < |x.ofLp 0| ∨ r < |x.ofLp 1|}

theorem Schoenflies.Plane.isConnected_beyondSquare (r : ℝ) : IsConnected (beyondSquare r)

The outside of a square is connected.

Four half-planes, each convex and hence connected, with consecutive ones sharing a corner. No polar decomposition, and no arbitrary union of connected sets. The radius needs no sign condition: for r < 0 the four half-planes already cover the plane.