English
Let s be a closed nonempty subset of the product space Πn E_n, where each E_n is a discrete-topology space. Then there exists a 1-Lipschitz map f from the whole product to itself whose image is exactly s and which fixes every point of s (i.e., f(x)=x for all x in s).
Русский
Пусть s — замкнутое ненулевое подмножество произведения Πn E_n, где каждая E_n — дискретное пространство. Тогда существует отображение f: Πn E_n → Πn E_n такое, что: (i) f(x)=x для всех x∈s; (ii) образ f равен s; (iii) f является 1-Липшицевым.
LaTeX
$$$\\\\exists f:(\\\\forall n, E n) \\\\to (\\\\forall n, E n), \\\\left( \\\\forall x \\\\in s, f x = x \\\\right) \\\\land \\\\text{range } f = s \\\\land \\\\text{LipschitzWith } 1 f$$$
Lean4
/-- Given a closed nonempty subset `s` of `Π (n : ℕ), E n`, there exists a Lipschitz retraction
onto this set, i.e., a Lipschitz map with range equal to `s`, equal to the identity on `s`. -/
theorem exists_lipschitz_retraction_of_isClosed {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty) :
∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ LipschitzWith 1 f := by
/- The map `f` is defined as follows. For `x ∈ s`, let `f x = x`. Otherwise, consider the longest
prefix `w` that `x` shares with an element of `s`, and let `f x = z_w` where `z_w` is an element
of `s` starting with `w`. All the desired properties are clear, except the fact that `f` is
`1`-Lipschitz: if two points `x, y` belong to a common cylinder of length `n`, one should show
that their images also belong to a common cylinder of length `n`. This is a case analysis:
* if both `x, y ∈ s`, then this is clear.
* if `x ∈ s` but `y ∉ s`, then the longest prefix `w` of `y` shared by an element of `s` is of
length at least `n` (because of `x`), and then `f y` starts with `w` and therefore stays in the
same length `n` cylinder.
* if `x ∉ s`, `y ∉ s`, let `w` be the longest prefix of `x` shared by an element of `s`. If its
length is `< n`, then it is also the longest prefix of `y`, and we get `f x = f y = z_w`.
Otherwise, `f x` remains in the same `n`-cylinder as `x`. Similarly for `y`. Finally, `f x` and
`f y` are again in the same `n`-cylinder, as desired. -/
classical
set f := fun x => if x ∈ s then x else (inter_cylinder_longestPrefix_nonempty hs hne x).some
have fs : ∀ x ∈ s, f x = x := fun x xs => by simp [f, xs]
refine
⟨f, fs, ?_, ?_⟩
-- check that the range of `f` is `s`.
· apply Subset.antisymm
· rintro x ⟨y, rfl⟩
by_cases hy : y ∈ s
· rwa [fs y hy]
simpa [f, if_neg hy] using (inter_cylinder_longestPrefix_nonempty hs hne y).choose_spec.1
· intro x hx
rw [← fs x hx]
exact
mem_range_self
_
-- check that `f` is `1`-Lipschitz, by a case analysis.
· refine
LipschitzWith.mk_one fun x y =>
?_
-- exclude the trivial cases where `x = y`, or `f x = f y`.
rcases eq_or_ne x y with (rfl | hxy)
· simp
rcases eq_or_ne (f x) (f y) with (h' | hfxfy)
· simp [h']
have I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y) :=
by
rw [← mem_cylinder_iff_eq]
apply mem_cylinder_firstDiff
suffices firstDiff x y ≤ firstDiff (f x) (f y) by
simpa [dist_eq_of_ne hxy, dist_eq_of_ne hfxfy]
-- case where `x ∈ s`
by_cases xs : x ∈ s
· rw [fs x
xs] at hfxfy
⊢
-- case where `y ∈ s`, trivial
by_cases ys : y ∈ s
·
rw [fs y ys]
-- case where `y ∉ s`
have A : (s ∩ cylinder y (longestPrefix y s)).Nonempty := inter_cylinder_longestPrefix_nonempty hs hne y
have fy : f y = A.some := by simp_rw [f, if_neg ys]
have I : cylinder A.some (firstDiff x y) = cylinder y (firstDiff x y) :=
by
rw [← mem_cylinder_iff_eq, firstDiff_comm]
apply cylinder_anti y _ A.some_mem.2
exact firstDiff_le_longestPrefix hs ys xs
rwa [← fy, ← I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy.symm, firstDiff_comm _ x] at I
· by_cases ys : y ∈ s
· have A : (s ∩ cylinder x (longestPrefix x s)).Nonempty := inter_cylinder_longestPrefix_nonempty hs hne x
have fx : f x = A.some := by simp_rw [f, if_neg xs]
have I : cylinder A.some (firstDiff x y) = cylinder x (firstDiff x y) :=
by
rw [← mem_cylinder_iff_eq]
apply cylinder_anti x _ A.some_mem.2
apply firstDiff_le_longestPrefix hs xs ys
rw [fs y ys] at hfxfy ⊢
rwa [← fx, I2, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at I
· have Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty := inter_cylinder_longestPrefix_nonempty hs hne x
have fx : f x = Ax.some := by simp_rw [f, if_neg xs]
have Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty := inter_cylinder_longestPrefix_nonempty hs hne y
have fy : f y = Ay.some := by
simp_rw [f, if_neg ys]
-- case where the common prefix to `x` and `s`, or `y` and `s`, is shorter than the
-- common part to `x` and `y` -- then `f x = f y`.
by_cases H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
· have : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s) :=
by
rcases H with H | H
· exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H xs ys
· symm
rw [firstDiff_comm] at H
exact cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff hs hne H ys xs
rw [fx, fy] at hfxfy
apply (hfxfy _).elim
congr
-- case where the common prefix to `x` and `s` is long, as well as the common prefix to
-- `y` and `s`. Then all points remain in the same cylinders.
· push_neg at H
have I1 : cylinder Ax.some (firstDiff x y) = cylinder x (firstDiff x y) :=
by
rw [← mem_cylinder_iff_eq]
exact cylinder_anti x H.1 Ax.some_mem.2
have I3 : cylinder y (firstDiff x y) = cylinder Ay.some (firstDiff x y) :=
by
rw [eq_comm, ← mem_cylinder_iff_eq]
exact cylinder_anti y H.2 Ay.some_mem.2
have : cylinder Ax.some (firstDiff x y) = cylinder Ay.some (firstDiff x y) := by rw [I1, I2, I3]
rw [← fx, ← fy, ← mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff hfxfy] at this
exact this
