[Merged by Bors] - feat(analysis/convex/topology): Separating by convex sets

[YaelDillies]

When s is compact, t is closed and both are convex, we can find disjoint open convex sets containing s and t.

---

• depends on: [Merged by Bors] - feat(analysis/normed_space/pointwise): Addition of balls #13381

[kkytola]

It is true that to use this for the proof of existence of disjoint thickenings, one hits the usual ennreal-hurdles. But it does imply that result, for example as follows. I'm not sure if others would consider this satisfactory as an approach. If it is acceptable in principle, then golfing and adding ennreal-lemmas may be worthwhile.

import topology.metric_space.hausdorff_distance

open nnreal ennreal set metric emetric filter

open_locale ennreal

variables {X : Type*} [pseudo_emetric_space X]

lemma suggested_lemma (K F : set X) (K_cpt : is_compact K) (K_nonempty : K.nonempty) :
  ∃ (x ∈ K), ∀ (x' ∈ K), inf_edist x F ≤ inf_edist x' F :=
K_cpt.exists_forall_le K_nonempty (@continuous_inf_edist _ _ F).continuous_on

lemma suggested_corollary {K F : set X} (K_cpt : is_compact K) (K_nonempty : K.nonempty) (F_closed : is_closed F) (disj : K ∩ F = ∅) :
 ∃ r > 0, ∀ (x ∈ K) (y ∈ F), r ≤ edist x y :=
begin
  rcases suggested_lemma K F K_cpt K_nonempty with ⟨x₀, ⟨x₀_in_K, h⟩⟩,
  set r := inf_edist x₀ F with def_r,
  refine ⟨r, _, _⟩,
  { by_contra r_vanish,
    rw [not_lt, nonpos_iff_eq_zero] at r_vanish,
    rw r_vanish at def_r,
    have x₀_also_mem := mem_closure_iff_inf_edist_zero.mpr def_r.symm,
    rw F_closed.closure_eq at x₀_also_mem,
    have oops : x₀ ∈ K ∩ F, from ⟨x₀_in_K, x₀_also_mem⟩,
    rw disj at oops,
    exact not_mem_empty x₀ oops, },
  { intros x x_in_K y y_in_F,
    exact le_inf_edist.mp (h x x_in_K) y y_in_F, },
end

lemma exists_disjoint_thickenings {K F : set X} (K_cpt : is_compact K)
  (F_closed : is_closed F) (disj : K ∩ F = ∅) :
  ∃ δ, 0 < δ ∧ disjoint (thickening δ K) (thickening δ F) :=
begin
  by_cases K_empty : K = ∅,
  { refine ⟨1, zero_lt_one, _⟩,
    rw [K_empty, thickening_empty],
    exact (thickening 1 F).empty_disjoint, },
  have K_nonempty : K.nonempty, from ne_empty_iff_nonempty.mp K_empty,
  rcases suggested_corollary K_cpt K_nonempty F_closed disj with ⟨r, r_pos, h⟩,
  set δ := (min 1 (r/2)).to_real with def_δ,
  have δ_pos : 0 < δ,
  { -- Given r_pos and def_δ, one would expect this to be a one-liner.
    apply (to_real_lt_to_real zero_ne_top 
           (lt_of_le_of_lt (min_le_left 1 (r/2)) one_lt_top).ne).mpr,
    apply lt_min ennreal.zero_lt_one _,
    rw div_eq_mul_inv,
    exact ennreal.mul_pos (ne_of_gt r_pos) (ennreal.inv_pos.mpr two_ne_top).ne.symm, },
  have two_δ : 2 * ennreal.of_real δ ≤ r, 
  { -- Given def_δ, one would expect this to be a one-liner at most!
    have obs := (@of_real_to_real_le (min 1 (r/2))).trans (min_le_right _ _),
    rw ←def_δ at obs,
    have got_it := ennreal.mul_le_mul (show (2 : ℝ≥0∞) ≤ 2, by simp only [le_refl]) obs,
    rwa ennreal.mul_div_cancel' two_ne_zero' two_ne_top at got_it, },
  refine ⟨δ, δ_pos, _⟩,
  by_contra overlap,
  rw not_disjoint_iff_nonempty_inter at overlap,
  rcases nonempty_def.mp overlap with ⟨z, ⟨z_near_K, z_near_F⟩⟩,
  rw mem_thickening_iff_exists_edist_lt at *,
  rcases z_near_K with ⟨x, ⟨x_in_K, z_near_x⟩⟩,
  rcases z_near_F with ⟨y, ⟨y_in_F, z_near_y⟩⟩,
  have tri := edist_triangle x z y,
  rw edist_comm x z at tri,
  have oops := lt_of_le_of_lt tri (ennreal.add_lt_add z_near_x z_near_y),
  rw [← mul_two, mul_comm] at oops,
  have oh_no := lt_of_lt_of_le oops two_δ,
  exact (lt_iff_not_ge _ _).mp oh_no (h x x_in_K y y_in_F),
end

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - feat(analysis/normed_space/pointwise): Addition of balls #13381
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests