feat(measure_theory/lebesgue_measure): volume s ≤ diam s (#8437)

* for `s : set real`, `volume s ≤ diam s`;
* for `s : set (ι → real)`, `volume s ≤ ∏ i, diam (eval i '' s) ≤ diam s ^ fintype.card ι`.

src/measure_theory/lebesgue_measure.lean

@@ -12,7 +12,7 @@ import measure_theory.pi
 noncomputable theory
 open classical set filter
 open ennreal (of_real)
-open_locale big_operators ennreal
+open_locale big_operators ennreal nnreal
 
 namespace measure_theory
 
@@ -336,6 +336,31 @@ lemma volume_pi_Ico {a b : ι → ℝ} :
   (volume (pi univ (λ i, Ico (a i) (b i)))).to_real = ∏ i, (b i - a i) :=
 by simp only [volume_pi_Ico, ennreal.to_real_prod, ennreal.to_real_of_real (sub_nonneg.2 (h _))]
 
+lemma volume_le_diam (s : set ℝ) : volume s ≤ emetric.diam s :=
+begin
+  by_cases hs : metric.bounded s,
+  { rw [real.ediam_eq hs, ← volume_Icc],
+    exact volume.mono (real.subset_Icc_Inf_Sup_of_bounded hs) },
+  { rw metric.ediam_of_unbounded hs, exact le_top }
+end
+
+lemma volume_pi_le_prod_diam (s : set (ι → ℝ)) :
+  volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) :=
+calc volume s ≤ volume (pi univ (λ i, closure (function.eval i '' s))) :
+  volume.mono $ subset.trans (subset_pi_eval_image univ s) $ pi_mono $ λ i hi, subset_closure
+          ... = ∏ i, volume (closure $ function.eval i '' s) :
+  volume_pi_pi _ $ λ i, measurable_set_closure
+          ... ≤ ∏ i : ι, emetric.diam (function.eval i '' s) :
+  finset.prod_le_prod' $ λ i hi, (volume_le_diam _).trans_eq (emetric.diam_closure _)
+
+lemma volume_pi_le_diam_pow (s : set (ι → ℝ)) :
+  volume s ≤ emetric.diam s ^ fintype.card ι :=
+calc volume s ≤ ∏ i : ι, emetric.diam (function.eval i '' s) : volume_pi_le_prod_diam s
+          ... ≤ ∏ i : ι, (1 : ℝ≥0) * emetric.diam s                      :
+  finset.prod_le_prod' $ λ i hi, (lipschitz_with.eval i).ediam_image_le s
+          ... = emetric.diam s ^ fintype.card ι              :
+  by simp only [ennreal.coe_one, one_mul, finset.prod_const, fintype.card]
+
 /-!
 ### Images of the Lebesgue measure under translation/multiplication/...
 -/

src/topology/metric_space/basic.lean

@@ -1709,13 +1709,13 @@ bounded_iff_ediam_ne_top.1 h
 lemma dist_le_diam_of_mem (h : bounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s :=
 dist_le_diam_of_mem' h.ediam_ne_top hx hy
 
+lemma ediam_of_unbounded (h : ¬(bounded s)) : emetric.diam s = ∞ :=
+by rwa [bounded_iff_ediam_ne_top, not_not] at h
+
 /-- An unbounded set has zero diameter. If you would prefer to get the value ∞, use `emetric.diam`.
 This lemma makes it possible to avoid side conditions in some situations -/
 lemma diam_eq_zero_of_unbounded (h : ¬(bounded s)) : diam s = 0 :=
-begin
-  simp only [bounded_iff_ediam_ne_top, not_not, ne.def] at h,
-  simp [diam, h]
-end
+by rw [diam, ediam_of_unbounded h, ennreal.top_to_real]
 
 /-- If `s ⊆ t`, then the diameter of `s` is bounded by that of `t`, provided `t` is bounded. -/
 lemma diam_mono {s t : set α} (h : s ⊆ t) (ht : bounded t) : diam s ≤ diam t :=

src/topology/metric_space/emetric_space.lean

@@ -457,6 +457,10 @@ lemma edist_pi_def [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) :
 lemma edist_pi_const [nonempty β] (a b : α) :
   edist (λ x : β, a) (λ _, b) = edist a b := finset.sup_const univ_nonempty (edist a b)
 
+lemma edist_le_pi_edist [Π b, pseudo_emetric_space (π b)] (f g : Π b, π b) (b : β) :
+  edist (f b) (g b) ≤ edist f g :=
+finset.le_sup (finset.mem_univ b)
+
 end pi
 
 namespace emetric

src/topology/metric_space/lipschitz.lean

@@ -153,6 +153,10 @@ lipschitz_with.of_edist_le $ assume x y, le_refl _
 protected lemma subtype_coe (s : set α) : lipschitz_with 1 (coe : s → α) :=
 lipschitz_with.subtype_val s
 
+protected lemma eval {α : ι → Type u} [Π i, pseudo_emetric_space (α i)] [fintype ι] (i : ι) :
+  lipschitz_with 1 (function.eval i : (Π i, α i) → α i) :=
+lipschitz_with.of_edist_le $ λ f g, by convert edist_le_pi_edist f g i
+
 protected lemma restrict (hf : lipschitz_with K f) (s : set α) :
   lipschitz_with K (s.restrict f) :=
 λ x y, hf x y