feat(analysis/convex/body): endow with Hausdorff metric (#16338)

Endows the type of convex bodies with the Hausdorff pseudo-metric.
If the underlying vector space is normed instead of only seminormed, this gives rise to the Hausdorff metric.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/analysis/convex/body.lean

@@ -4,23 +4,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul A. Reichert
 -/
 import analysis.convex.basic
-import data.real.nnreal
-import topology.algebra.module.basic
-import topology.instances.real
+import analysis.normed_space.basic
+import topology.metric_space.hausdorff_distance
 
 /-!
-# convex bodies
+# Convex bodies
 
 This file contains the definition of the type `convex_body V`
 consisting of
 convex, compact, nonempty subsets of a real topological vector space `V`.
 
-`convex_body V` is a module over the nonnegative reals (`nnreal`).
+`convex_body V` is a module over the nonnegative reals (`nnreal`) and a pseudo-metric space.
+If `V` is a normed space, `convex_body V` is a metric space.
+
+## TODO
 
-TODOs:
-- endow it with the Hausdorff metric
 - define positive convex bodies, requiring the interior to be nonempty
 - introduce support sets
+- Characterise the interaction of the distance with algebraic operations, eg
+  `dist (a • K) (a • L) = ‖a‖ * dist K L`, `dist (a +ᵥ K) (a +ᵥ L) = dist K L`
 
 ## Tags
 
@@ -30,37 +32,39 @@ convex, convex body
 open_locale pointwise
 open_locale nnreal
 
-variables (V : Type*) [topological_space V] [add_comm_group V] [has_continuous_add V]
-  [module ℝ V] [has_continuous_smul ℝ V]
+variables {V : Type*}
 
 /--
 Let `V` be a real topological vector space. A subset of `V` is a convex body if and only if
 it is convex, compact, and nonempty.
 -/
-structure convex_body :=
+structure convex_body (V : Type*) [topological_space V] [add_comm_monoid V] [has_smul ℝ V] :=
 (carrier : set V)
 (convex' : convex ℝ carrier)
 (is_compact' : is_compact carrier)
 (nonempty' : carrier.nonempty)
 
 namespace convex_body
-
-variables {V}
+section TVS
+variables [topological_space V] [add_comm_group V] [module ℝ V]
 
 instance : set_like (convex_body V) V :=
 { coe := convex_body.carrier,
   coe_injective' := λ K L h, by { cases K, cases L, congr' } }
 
-lemma convex (K : convex_body V) : convex ℝ (K : set V) := K.convex'
-lemma is_compact (K : convex_body V) : is_compact (K : set V) := K.is_compact'
-lemma nonempty (K : convex_body V) : (K : set V).nonempty := K.nonempty'
+protected lemma convex (K : convex_body V) : convex ℝ (K : set V) := K.convex'
+protected lemma is_compact (K : convex_body V) : is_compact (K : set V) := K.is_compact'
+protected lemma nonempty (K : convex_body V) : (K : set V).nonempty := K.nonempty'
 
 @[ext]
 protected lemma ext {K L : convex_body V} (h : (K : set V) = L) : K = L := set_like.ext' h
 
 @[simp]
 lemma coe_mk (s : set V) (h₁ h₂ h₃) : (mk s h₁ h₂ h₃ : set V) = s := rfl
 
+section has_continuous_add
+variables [has_continuous_add V]
+
 instance : add_monoid (convex_body V) :=
 -- we cannot write K + L to avoid reducibility issues with the set.has_add instance
 { add := λ K L, ⟨set.image2 (+) K L,
@@ -84,12 +88,18 @@ instance : add_comm_monoid (convex_body V) :=
 { add_comm := λ K L, by { ext, simp only [coe_add, add_comm] },
   .. convex_body.add_monoid }
 
+end has_continuous_add
+
+variables [has_continuous_smul ℝ V]
+
 instance : has_smul ℝ (convex_body V) :=
 { smul := λ c K, ⟨c • (K : set V), K.convex.smul _, K.is_compact.smul _, K.nonempty.smul_set⟩ }
 
 @[simp]
 lemma coe_smul (c : ℝ) (K : convex_body V) : (↑(c • K) : set V) = c • (K : set V) := rfl
 
+variables [has_continuous_add V]
+
 instance : distrib_mul_action ℝ (convex_body V) :=
 { to_has_smul := convex_body.has_smul,
   one_smul := λ K, by { ext, simp only [coe_smul, one_smul] },
@@ -112,4 +122,41 @@ instance : module ℝ≥0 (convex_body V) :=
   end,
   zero_smul := λ K, by { ext1, exact set.zero_smul_set K.nonempty } }
 
+end TVS
+
+section seminormed_add_comm_group
+variables [seminormed_add_comm_group V] [normed_space ℝ V] (K L : convex_body V)
+
+protected lemma bounded : metric.bounded (K : set V) := K.is_compact.bounded
+
+lemma Hausdorff_edist_ne_top {K L : convex_body V} : emetric.Hausdorff_edist (K : set V) L ≠ ⊤ :=
+by apply_rules [metric.Hausdorff_edist_ne_top_of_nonempty_of_bounded, convex_body.nonempty,
+  convex_body.bounded]
+
+/-- Convex bodies in a fixed seminormed space $V$ form a pseudo-metric space under the Hausdorff
+metric. -/
+noncomputable instance : pseudo_metric_space (convex_body V) :=
+{ dist := λ K L, metric.Hausdorff_dist (K : set V) L,
+  dist_self := λ _, metric.Hausdorff_dist_self_zero,
+  dist_comm := λ _ _, metric.Hausdorff_dist_comm,
+  dist_triangle := λ K L M, metric.Hausdorff_dist_triangle Hausdorff_edist_ne_top }
+
+@[simp, norm_cast]
+lemma Hausdorff_dist_coe : metric.Hausdorff_dist (K : set V) L = dist K L := rfl
+
+@[simp, norm_cast] lemma Hausdorff_edist_coe : emetric.Hausdorff_edist (K : set V) L = edist K L :=
+by { rw edist_dist, exact (ennreal.of_real_to_real Hausdorff_edist_ne_top).symm }
+
+end seminormed_add_comm_group
+
+section normed_add_comm_group
+variables [normed_add_comm_group V] [normed_space ℝ V]
+
+/-- Convex bodies in a fixed normed space `V` form a metric space under the Hausdorff metric. -/
+noncomputable instance : metric_space (convex_body V) :=
+{ eq_of_dist_eq_zero := λ K L hd, convex_body.ext $
+    (K.is_compact.is_closed.Hausdorff_dist_zero_iff_eq
+      L.is_compact.is_closed Hausdorff_edist_ne_top).mp hd }
+
+end normed_add_comm_group
 end convex_body