Moving an interior point of the square

The pointed form of the bounded theorem needs a self-homeomorphism of the closed square that fixes the boundary pointwise and carries one prescribed interior point to another. The blueprint builds it by coning: the four triangles conv {x, vᵢ, vᵢ₊₁} triangulate the square, and the affine map of each onto conv {y, vᵢ, vᵢ₊₁} fixing the two corners pastes with its neighbours along the radial edges.

The construction here is the same map in different coordinates, and it is written so that no pasting of four affine pieces is needed. It is the composite of two shears. A shear bends one coordinate by the piecewise-linear self-map of [-r, r] that fixes the two endpoints and moves a chosen breakpoint (bend), with a displacement that is scaled by a tent function of the other coordinate (tent), so that it dies away to zero on the two transverse sides of the square. The first shear moves the first coordinate of x to that of y, the second moves the second coordinate.

Two features make this cheap. Writing the tent as a minimum of two affine functions makes it continuous with no case split at all. And the family of shears is closed under inversion: the shear with displacement parameters k, k' is undone by the shear with parameters k + k', -k', so bijectivity and the continuity of the inverse come from one composition identity (bend_bend) instead of from a compactness argument, and no map has to be inverted by hand.

Blueprint

• Plane.exists_squareMover — Lemma (Moving an interior point of the square): for interior points x, y of the square there are mutually inverse boundary-fixing self-maps M, N of the closed square with M x = y. Plane.IsSquareMover bundles the properties that make M a homeomorphism of the square onto itself, Plane.IsSquareMover.homeomorph repackages it as a Homeomorph, and Plane.IsSquareMover.eqOn_frontier states the boundary condition against the topological frontier, which Plane.frontier_closedSquare identifies with the blueprint's boundary square S.
• Plane.iInter_eq_singleton_of_mem_tail — the point-set kernel of Proposition (Skeleton agreement). The proposition itself is not statable in the present development; see the section comment at that lemma for exactly what is and is not proved.

Supporting material, of independent use: Plane.tent and Plane.bend with their algebra, Plane.continuousOn_bend, the coordinate lemmas Plane.abs_sub_le_supDist, Plane.supDist_le_of_forall, Plane.exists_abs_sub_eq_of_supDist_eq, and Plane.interior_closedSquare.

The tent function

noncomputable def Schoenflies.Plane.tent (r p u : ℝ) : ℝ

The tent of height 1 on [-r, r] with peak at p: it vanishes at the two endpoints, takes the value 1 at p, and is linear on either side. Written as a minimum of two affine functions rather than as a case split, which makes its continuity immediate.

Equations

• Schoenflies.Plane.tent r p u = min ((u + r) / (p + r)) ((r - u) / (r - p))

theorem Schoenflies.Plane.continuous_tent (r p : ℝ) : Continuous (tent r p)

theorem Schoenflies.Plane.pos_of_lt_lt {r p : ℝ} (h₁ : -r < p) (h₂ : p < r) : 0 < r

theorem Schoenflies.Plane.tent_le_one {r p : ℝ} (h₁ : -r < p) (h₂ : p < r) (u : ℝ) : tent r p u ≤ 1

theorem Schoenflies.Plane.tent_nonneg {r p u : ℝ} (h₁ : -r < p) (h₂ : p < r) (hu : -r ≤ u) (hu' : u ≤ r) : 0 ≤ tent r p u

@[simp]

theorem Schoenflies.Plane.tent_self {r p : ℝ} (h₁ : -r < p) (h₂ : p < r) : tent r p p = 1

theorem Schoenflies.Plane.tent_left {r p : ℝ} (h₁ : -r < p) (h₂ : p < r) : tent r p (-r) = 0

theorem Schoenflies.Plane.tent_right {r p : ℝ} (h₁ : -r < p) (h₂ : p < r) : tent r p r = 0

Bending an interval

noncomputable def Schoenflies.Plane.bend (r p q u : ℝ) : ℝ

The piecewise-linear self-map of [-r, r] that fixes both endpoints and carries p to q, linearly on [-r, p] and on [p, r].

Equations

• Schoenflies.Plane.bend r p q u = if u ≤ p then -r + (u + r) * (q + r) / (p + r) else r - (r - u) * (r - q) / (r - p)

theorem Schoenflies.Plane.bend_of_le {r p q u : ℝ} (h : u ≤ p) : bend r p q u = -r + (u + r) * (q + r) / (p + r)

theorem Schoenflies.Plane.bend_of_gt {r p q u : ℝ} (h : p < u) : bend r p q u = r - (r - u) * (r - q) / (r - p)

theorem Schoenflies.Plane.bend_left {r p q : ℝ} (h : -r ≤ p) : bend r p q (-r) = -r

theorem Schoenflies.Plane.bend_right {r p q : ℝ} (h : p < r) : bend r p q r = r

theorem Schoenflies.Plane.bend_self {r p q : ℝ} (h : -r < p) : bend r p q p = q

theorem Schoenflies.Plane.bend_refl {r p : ℝ} (h₁ : -r < p) (h₂ : p < r) (u : ℝ) : bend r p p u = u

theorem Schoenflies.Plane.bend_le_of_le {r p q u : ℝ} (h₁ : -r < p) (h₂ : -r < q) (h : u ≤ p) : bend r p q u ≤ q

On the left half, the bend does not go past the image q of the peak.

theorem Schoenflies.Plane.lt_bend_of_lt {r p q u : ℝ} (h₁ : p < r) (h₂ : q < r) (h : p < u) : q < bend r p q u

On the right half, the bend stays past the image q of the peak.

theorem Schoenflies.Plane.bend_mem {r p q u : ℝ} (h₁ : -r < p) (h₂ : p < r) (h₃ : -r < q) (h₄ : q < r) (hu : -r ≤ u) (hu' : u ≤ r) : -r ≤ bend r p q u ∧ bend r p q u ≤ r

The bend maps [-r, r] into itself.

theorem Schoenflies.Plane.bend_bend {r p q : ℝ} (h₁ : -r < p) (h₂ : p < r) (h₃ : -r < q) (h₄ : q < r) (u : ℝ) : bend r q p (bend r p q u) = u

Bending from p to q and back from q to p is the identity.

theorem Schoenflies.Plane.bend_eq_right {r p q u : ℝ} (h₁ : p + r ≠ 0) (h₂ : r - p ≠ 0) (h : p ≤ u) : bend r p q u = r - (r - u) * (r - q) / (r - p)

Past the peak the right-hand branch of the bend is valid, including at the peak itself, where the two branches agree.

theorem Schoenflies.Plane.continuousOn_bend (r : ℝ) {s : Set Plane} {P Q U : Plane → ℝ} (hs : IsClosed s) (hP : Continuous P) (hQ : Continuous Q) (hU : Continuous U) (h1 : ∀ z ∈ s, P z + r ≠ 0) (h2 : ∀ z ∈ s, r - P z ≠ 0) : ContinuousOn (fun (z : Plane) => bend r (P z) (Q z) (U z)) s

Continuity of a bend whose three arguments vary continuously, on a closed set where the peak stays away from the two endpoints. The two branches are pasted along the closed sets where the argument is on one or the other side of the peak.

Coordinates of the square

theorem Schoenflies.Plane.abs_sub_le_supDist (z c : Plane) (l : Fin 2) : |z.ofLp l - c.ofLp l| ≤ z.supDist c

Each coordinate difference is bounded by the sup distance.

theorem Schoenflies.Plane.supDist_le_of_forall {z c : Plane} {r : ℝ} (h : ∀ (l : Fin 2), |z.ofLp l - c.ofLp l| ≤ r) : z.supDist c ≤ r

Conversely, a bound on both coordinate differences bounds the sup distance.

theorem Schoenflies.Plane.exists_abs_sub_eq_of_supDist_eq {z c : Plane} {r : ℝ} (h : z.supDist c = r) : ∃ (l : Fin 2), |z.ofLp l - c.ofLp l| = r

The sup distance is attained at one of the two coordinates.

theorem Schoenflies.Plane.abs_sub_lt_of_mem_openSquare {z c : Plane} {r : ℝ} (hz : z ∈ c.openSquare r) (l : Fin 2) : |z.ofLp l - c.ofLp l| < r

theorem Schoenflies.Plane.mem_Ioo_of_mem_openSquare {z c : Plane} {r : ℝ} (hz : z ∈ c.openSquare r) (l : Fin 2) : z.ofLp l - c.ofLp l ∈ Set.Ioo (-r) r

The coordinate of a point of the open square, as a member of the open interval.

theorem Schoenflies.Plane.fin2_eq_of_ne_of_ne {i j l : Fin 2} (h₁ : j ≠ i) (h₂ : l ≠ i) : l = j

In Fin 2, two indices distinct from a third are equal.

Shearing the square along one coordinate

noncomputable def Schoenflies.Plane.shearWeight (c : Plane) (r b : ℝ) (j : Fin 2) (z : Plane) : ℝ

The weight of the level line of z transverse to the i-th coordinate: it is 1 on the level b and dies away to 0 at the two sides z j - c j = ±r of the square.

Equations

• c.shearWeight r b j z = Schoenflies.Plane.tent r b (z.ofLp j - c.ofLp j)

noncomputable def Schoenflies.Plane.shear (c : Plane) (r a b k k' : ℝ) (i j : Fin 2) (z : Plane) : Plane

The shear of the square about c of radius r in the direction of the i-th coordinate. On the level line indexed by w = shearWeight, the i-th coordinate is bent by the piecewise-linear map carrying a + k * w to a + (k + k') * w and fixing the two sides z i - c i = ±r. Both the map with parameters k, k' and its inverse, which has parameters k + k', -k', belong to this two-parameter family — that is what the second parameter is for.

Equations

• One or more equations did not get rendered due to their size.

structure Schoenflies.Plane.IsShear (r a b k k' : ℝ) : Prop

The parameters of a shear are admissible when the peak of the level weight and the peak of every bend it performs stay strictly inside the square.

• peak : b ∈ Set.Ioo (-r) r

  the level of maximal displacement is interior

• base : a ∈ Set.Ioo (-r) r

  the point that is moved is interior

• mid : a + k ∈ Set.Ioo (-r) r

  the breakpoints of the bends are interior

• top : a + (k + k') ∈ Set.Ioo (-r) r

  the images of the breakpoints are interior

theorem Schoenflies.Plane.IsShear.inv {r a b k k' : ℝ} (h : IsShear r a b k k') : IsShear r a b (k + k') (-k')

The inverse shear has admissible parameters as well.

theorem Schoenflies.Plane.shear_apply_same {r : ℝ} {c : Plane} {a b k k' : ℝ} {i j : Fin 2} {z : Plane} : (c.shear r a b k k' i j z).ofLp i = c.ofLp i + bend r (a + k * c.shearWeight r b j z) (a + (k + k') * c.shearWeight r b j z) (z.ofLp i - c.ofLp i)

theorem Schoenflies.Plane.shear_apply_ne {r : ℝ} {c : Plane} {a b k k' : ℝ} {i j l : Fin 2} {z : Plane} (h : l ≠ i) : (c.shear r a b k k' i j z).ofLp l = z.ofLp l

theorem Schoenflies.Plane.mem_Ioo_of_weight {r a k w : ℝ} (ha : a ∈ Set.Ioo (-r) r) (hak : a + k ∈ Set.Ioo (-r) r) (hw : w ∈ Set.Icc 0 1) : a + k * w ∈ Set.Ioo (-r) r

A convex combination of two interior points of (-r, r) is interior.

theorem Schoenflies.Plane.shearWeight_mem {r : ℝ} {c : Plane} {a b k k' : ℝ} {j : Fin 2} {z : Plane} (h : IsShear r a b k k') (hz : z ∈ c.closedSquare r) : c.shearWeight r b j z ∈ Set.Icc 0 1

On the square, the level weight is a weight.

theorem Schoenflies.Plane.shear_mid_mem {r : ℝ} {c : Plane} {a b k k' : ℝ} {j : Fin 2} {z : Plane} (h : IsShear r a b k k') (hz : z ∈ c.closedSquare r) : a + k * c.shearWeight r b j z ∈ Set.Ioo (-r) r

On the square, the breakpoint of the bend performed by the shear is interior.

theorem Schoenflies.Plane.shear_top_mem {r : ℝ} {c : Plane} {a b k k' : ℝ} {j : Fin 2} {z : Plane} (h : IsShear r a b k k') (hz : z ∈ c.closedSquare r) : a + (k + k') * c.shearWeight r b j z ∈ Set.Ioo (-r) r

On the square, the image of the breakpoint is interior.

theorem Schoenflies.Plane.shear_mapsTo {r : ℝ} {c : Plane} {a b k k' : ℝ} (h : IsShear r a b k k') (i j : Fin 2) : Set.MapsTo (c.shear r a b k k' i j) (c.closedSquare r) (c.closedSquare r)

The shear maps the closed square to itself.

theorem Schoenflies.Plane.shear_shear {r : ℝ} {c : Plane} {a b k k' : ℝ} {i j : Fin 2} {z : Plane} (h : IsShear r a b k k') (hij : j ≠ i) (hz : z ∈ c.closedSquare r) : c.shear r a b (k + k') (-k') i j (c.shear r a b k k' i j z) = z

The shear with parameters k + k', -k' undoes the shear with parameters k, k'.

theorem Schoenflies.Plane.shear_eq_self_of_boundary {r : ℝ} {c : Plane} {a b k k' : ℝ} {i j : Fin 2} {z : Plane} (h : IsShear r a b k k') (hij : j ≠ i) (hz : z ∈ c.closedSquare r) (hbd : z.supDist c = r) : c.shear r a b k k' i j z = z

The shear fixes the boundary of the square pointwise.

theorem Schoenflies.Plane.shear_continuousOn {r : ℝ} {c : Plane} {a b k k' : ℝ} (h : IsShear r a b k k') (i j : Fin 2) : ContinuousOn (c.shear r a b k k' i j) (c.closedSquare r)

The shear is continuous on the square.

Movers of the square

structure Schoenflies.Plane.IsSquareMover (c : Plane) (r : ℝ) (M N : Plane → Plane) : Prop

M and N are mutually inverse self-homeomorphisms of the closed square about c of radius r, each fixing its boundary pointwise. This is the "homeomorphism of Q fixing S" of the blueprint, written without the Homeomorph bundle; IsSquareMover.homeomorph repackages it as one.

• mapsTo : Set.MapsTo M (c.closedSquare r) (c.closedSquare r)

  M maps the square to itself

• mapsTo_inv : Set.MapsTo N (c.closedSquare r) (c.closedSquare r)

  N maps the square to itself

• continuousOn : ContinuousOn M (c.closedSquare r)

  M is continuous on the square

• continuousOn_inv : ContinuousOn N (c.closedSquare r)

  N is continuous on the square

• invOn : Set.InvOn N M (c.closedSquare r) (c.closedSquare r)

  the two are mutually inverse there

• fixes (z : Plane) : z ∈ c.closedSquare r → z.supDist c = r → M z = z

  M fixes the boundary pointwise

• fixes_inv (z : Plane) : z ∈ c.closedSquare r → z.supDist c = r → N z = z

  N fixes the boundary pointwise

theorem Schoenflies.Plane.IsSquareMover.symm {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) : c.IsSquareMover r N M

theorem Schoenflies.Plane.IsSquareMover.bijOn {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) : Set.BijOn M (c.closedSquare r) (c.closedSquare r)

theorem Schoenflies.Plane.IsSquareMover.image_eq {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) : M '' c.closedSquare r = c.closedSquare r

theorem Schoenflies.Plane.IsSquareMover.comp {r : ℝ} {c : Plane} {M N M' N' : Plane → Plane} (h : c.IsSquareMover r M N) (h' : c.IsSquareMover r M' N') : c.IsSquareMover r (M' ∘ M) (N ∘ N')

Movers compose: M' after M, undone by N after N'.

theorem Schoenflies.Plane.isSquareMover_shear {r : ℝ} {c : Plane} {a b k k' : ℝ} {i j : Fin 2} (h : IsShear r a b k k') (hij : j ≠ i) : c.IsSquareMover r (c.shear r a b k k' i j) (c.shear r a b (k + k') (-k') i j)

A shear, together with the shear that undoes it, is a mover of the square.

Moving an interior point

theorem Schoenflies.Plane.exists_squareMover {c x y : Plane} {r : ℝ} (hx : x ∈ c.openSquare r) (hy : y ∈ c.openSquare r) : ∃ (M : Plane → Plane) (N : Plane → Plane), c.IsSquareMover r M N ∧ M x = y ∧ N y = x

Blueprint Lemma (Moving an interior point of the square). For any two interior points x and y of the closed square about c of radius r there is a self-homeomorphism of the square carrying x to y and fixing the boundary pointwise.

The map is built as two shears: the first moves the first coordinate of x to that of y along the level line of x, the second moves the second coordinate along the level line of the result. Each shear bends one coordinate by a piecewise-linear map whose displacement dies away to zero at the two transverse sides, which is exactly the piecewise-affine cone construction of the blueprint, written in coordinates.

The boundary of the square

theorem Schoenflies.Plane.add_smul_single_apply (z : Plane) (t : ℝ) (l : Fin 2) : (z + t • EuclideanSpace.single l 1).ofLp l = z.ofLp l + t

theorem Schoenflies.Plane.dist_add_smul_single (z : Plane) (t : ℝ) (l : Fin 2) : dist (z + t • EuclideanSpace.single l 1) z = |t|

theorem Schoenflies.Plane.interior_closedSquare (c : Plane) (r : ℝ) : interior (c.closedSquare r) = c.openSquare r

The interior of the closed square is the open square: a point with a coordinate at distance exactly r from the centre can be pushed further out along that coordinate.

theorem Schoenflies.Plane.frontier_closedSquare (c : Plane) (r : ℝ) : frontier (c.closedSquare r) = {z : Plane | z.supDist c = r}

The boundary of the closed square is the sup-distance sphere: the blueprint's S.

theorem Schoenflies.Plane.IsSquareMover.eqOn_frontier {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) : Set.EqOn M id (frontier (c.closedSquare r))

A mover is the identity on the boundary square S.

The mover as a homeomorphism

noncomputable def Schoenflies.Plane.IsSquareMover.homeomorph {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) : ↑(c.closedSquare r) ≃ₜ ↑(c.closedSquare r)

A mover of the square, packaged as a self-homeomorphism of the closed square.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Schoenflies.Plane.IsSquareMover.homeomorph_apply {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) (z : ↑(c.closedSquare r)) : ↑(h.homeomorph z) = M ↑z

@[simp]

theorem Schoenflies.Plane.IsSquareMover.homeomorph_symm_apply {r : ℝ} {c : Plane} {M N : Plane → Plane} (h : c.IsSquareMover r M N) (z : ↑(c.closedSquare r)) : ↑(h.homeomorph.symm z) = N ↑z

The point-set kernel of skeleton agreement

The blueprint's Proposition (Skeleton agreement) says that the limit map F, defined at x as the unique point of the nested intersection ⋂ n, T n x of closed target stars, agrees with every finite skeleton map: if x ∈ G_N ∩ D then F x = g_N x. Its proof is one line of point-set topology once the combinatorics is in place — the value g_N x lies in T n x for every n ≥ N, hence in the intersection, hence is the point of the intersection.

That one line is what follows. The proposition itself cannot be stated in this development yet: matched cell structures, carriers, stars, the skeleton homeomorphisms g_n and the limit map F do not exist here. What is proved is exactly the implication the proposition rests on, with the nested stars as an abstract antitone sequence of shrinking compacta and g_N x as an abstract point of all late terms.

theorem Schoenflies.Plane.iInter_eq_singleton_of_mem_tail {K : ℕ → Set Plane} {v : Plane} {N : ℕ} (hne : ∀ (n : ℕ), (K n).Nonempty) (hK : ∀ (n : ℕ), IsCompact (K n)) (hmono : Antitone K) (hdiam : Filter.Tendsto (fun (n : ℕ) => Metric.diam (K n)) Filter.atTop (nhds 0)) (hv : ∀ (n : ℕ), N ≤ n → v ∈ K n) : ⋂ (n : ℕ), K n = {v}

If the terms of an antitone sequence of nonempty compacta have diameters tending to zero, and a point lies in every term from some index on, then that point is the unique point of the intersection. Blueprint Proposition (Skeleton agreement), stripped of the cell apparatus: read K n as the closed target star T n x and v as the skeleton value g_N x.