chore(analysis/convex): trivial generalizations of ℝ (#9298)

src/analysis/calculus/deriv.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sébastien Gouëzel
 -/
 import analysis.calculus.fderiv
+import data.polynomial.derivative
 
 /-!
 

src/analysis/calculus/local_extr.lean

@@ -7,6 +7,7 @@ import analysis.calculus.deriv
 import topology.algebra.ordered.extend_from
 import topology.algebra.polynomial
 import topology.local_extr
+import data.polynomial.field_division
 
 /-!
 # Local extrema of smooth functions

src/analysis/convex/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudriashov, Yaël Dillies
 -/
-import data.complex.module
+import algebra.order.smul
 import data.set.intervals.image_preimage
 import linear_algebra.affine_space.affine_map
 import order.closure
@@ -836,30 +836,6 @@ end
 end add_comm_monoid
 end linear_ordered_field
 
-lemma convex_halfspace_re_lt (r : ℝ) : convex ℝ {c : ℂ | c.re < r} :=
-convex_halfspace_lt (is_linear_map.mk complex.add_re complex.smul_re) _
-
-lemma convex_halfspace_re_le (r : ℝ) : convex ℝ {c : ℂ | c.re ≤ r} :=
-convex_halfspace_le (is_linear_map.mk complex.add_re complex.smul_re) _
-
-lemma convex_halfspace_re_gt (r : ℝ) : convex ℝ {c : ℂ | r < c.re } :=
-convex_halfspace_gt (is_linear_map.mk complex.add_re complex.smul_re) _
-
-lemma convex_halfspace_re_ge (r : ℝ) : convex ℝ {c : ℂ | r ≤ c.re} :=
-convex_halfspace_ge (is_linear_map.mk complex.add_re complex.smul_re) _
-
-lemma convex_halfspace_im_lt (r : ℝ) : convex ℝ {c : ℂ | c.im < r} :=
-convex_halfspace_lt (is_linear_map.mk complex.add_im complex.smul_im) _
-
-lemma convex_halfspace_im_le (r : ℝ) : convex ℝ {c : ℂ | c.im ≤ r} :=
-convex_halfspace_le (is_linear_map.mk complex.add_im complex.smul_im) _
-
-lemma convex_halfspace_im_gt (r : ℝ) : convex ℝ {c : ℂ | r < c.im} :=
-convex_halfspace_gt (is_linear_map.mk complex.add_im complex.smul_im) _
-
-lemma convex_halfspace_im_ge (r : ℝ) : convex ℝ {c : ℂ | r ≤ c.im} :=
-convex_halfspace_ge (is_linear_map.mk complex.add_im complex.smul_im) _
-
 /-!
 #### Convex sets in an ordered space
 Relates `convex` and `ord_connected`.
@@ -1055,25 +1031,25 @@ end add_comm_monoid
 end ordered_ring
 end convex_hull
 
-
-variables {ι ι' : Type*} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set E}
-
 /-! ### Simplex -/
 
 section simplex
 
-variables (ι) [fintype ι] {f : ι → ℝ}
+variables (ι : Type*) [fintype ι]
 
 /-- The standard simplex in the space of functions `ι → ℝ` is the set
 of vectors with non-negative coordinates with total sum `1`. -/
-def std_simplex (ι : Type*) [fintype ι] : set (ι → ℝ) :=
+def std_simplex (ι : Type*) [fintype ι] (R : Type*) [ordered_semiring R] :
+  set (ι → R) :=
 {f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1}
 
+variables (R : Type*) [ordered_semiring R] {f : ι → R}
+
 lemma std_simplex_eq_inter :
-  std_simplex ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1} :=
+  std_simplex ι R = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1} :=
 by { ext f, simp only [std_simplex, set.mem_inter_eq, set.mem_Inter, set.mem_set_of_eq] }
 
-lemma convex_std_simplex : convex ℝ (std_simplex ι) :=
+lemma convex_std_simplex : convex R (std_simplex ι R) :=
 begin
   refine λ f g hf hg a b ha hb hab, ⟨λ x, _, _⟩,
   { apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1] },
@@ -1084,7 +1060,7 @@ end
 
 variable {ι}
 
-lemma ite_eq_mem_std_simplex (i : ι) : (λ j, ite (i = j) (1:ℝ) 0) ∈ std_simplex ι :=
+lemma ite_eq_mem_std_simplex (i : ι) : (λ j, ite (i = j) (1:R) 0) ∈ std_simplex ι R :=
 ⟨λ j, by simp only; split_ifs; norm_num, by rw [finset.sum_ite_eq, if_pos (finset.mem_univ _)]⟩
 
 end simplex

src/analysis/convex/caratheodory.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin, Scott Morrison
 -/
 import analysis.convex.combination
 import linear_algebra.affine_space.independent
+import data.real.basic
 
 /-!
 # Carathéodory's convexity theorem

src/analysis/convex/combination.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudriashov
 -/
 import analysis.convex.basic
+import algebra.big_operators.order
 
 /-!
 # Convex combinations
@@ -25,15 +26,16 @@ open set
 open_locale big_operators classical
 
 universes u u'
-variables {E F ι ι' : Type*} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F]
+variables {R E F ι ι' : Type*}
+  [linear_ordered_field R] [add_comm_group E] [module R E] [add_comm_group F] [module R F]
   {s : set E}
 
 /-- Center of mass of a finite collection of points with prescribed weights.
 Note that we require neither `0 ≤ w i` nor `∑ w = 1`. -/
-noncomputable def finset.center_mass (t : finset ι) (w : ι → ℝ) (z : ι → E) : E :=
+def finset.center_mass (t : finset ι) (w : ι → R) (z : ι → E) : E :=
 (∑ i in t, w i)⁻¹ • (∑ i in t, w i • z i)
 
-variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι → ℝ) (z : ι → E)
+variables (i j : ι) (c : R) (t : finset ι) (w : ι → R) (z : ι → E)
 
 open finset
 
@@ -68,8 +70,8 @@ by simp only [finset.center_mass, finset.smul_sum, (mul_smul _ _ _).symm, mul_co
 /-- A convex combination of two centers of mass is a center of mass as well. This version
 deals with two different index types. -/
 lemma finset.center_mass_segment'
-  (s : finset ι) (t : finset ι') (ws : ι → ℝ) (zs : ι → E) (wt : ι' → ℝ) (zt : ι' → E)
-  (hws : ∑ i in s, ws i = 1) (hwt : ∑ i in t, wt i = 1) (a b : ℝ) (hab : a + b = 1) :
+  (s : finset ι) (t : finset ι') (ws : ι → R) (zs : ι → E) (wt : ι' → R) (zt : ι' → E)
+  (hws : ∑ i in s, ws i = 1) (hwt : ∑ i in t, wt i = 1) (a b : R) (hab : a + b = 1) :
   a • s.center_mass ws zs + b • t.center_mass wt zt =
     (s.map function.embedding.inl ∪ t.map function.embedding.inr).center_mass
       (sum.elim (λ i, a * ws i) (λ j, b * wt j))
@@ -84,16 +86,16 @@ end
 /-- A convex combination of two centers of mass is a center of mass as well. This version
 works if two centers of mass share the set of original points. -/
 lemma finset.center_mass_segment
-  (s : finset ι) (w₁ w₂ : ι → ℝ) (z : ι → E)
-  (hw₁ : ∑ i in s, w₁ i = 1) (hw₂ : ∑ i in s, w₂ i = 1) (a b : ℝ) (hab : a + b = 1) :
+  (s : finset ι) (w₁ w₂ : ι → R) (z : ι → E)
+  (hw₁ : ∑ i in s, w₁ i = 1) (hw₂ : ∑ i in s, w₂ i = 1) (a b : R) (hab : a + b = 1) :
   a • s.center_mass w₁ z + b • s.center_mass w₂ z =
     s.center_mass (λ i, a * w₁ i + b * w₂ i) z :=
 have hw : ∑ i in s, (a * w₁ i + b * w₂ i) = 1,
   by simp only [mul_sum.symm, sum_add_distrib, mul_one, *],
 by simp only [finset.center_mass_eq_of_sum_1, smul_sum, sum_add_distrib, add_smul, mul_smul, *]
 
 lemma finset.center_mass_ite_eq (hi : i ∈ t) :
-  t.center_mass (λ j, if (i = j) then 1 else 0) z = z i :=
+  t.center_mass (λ j, if (i = j) then (1 : R) else 0) z = z i :=
 begin
   rw [finset.center_mass_eq_of_sum_1],
   transitivity ∑ j in t, if (i = j) then z i else 0,
@@ -123,7 +125,7 @@ variable {z}
 
 /-- The center of mass of a finite subset of a convex set belongs to the set
 provided that all weights are non-negative, and the total weight is positive. -/
-lemma convex.center_mass_mem (hs : convex ℝ s) :
+lemma convex.center_mass_mem (hs : convex R s) :
   (∀ i ∈ t, 0 ≤ w i) → (0 < ∑ i in t, w i) → (∀ i ∈ t, z i ∈ s) → t.center_mass w z ∈ s :=
 begin
   induction t using finset.induction with i t hi ht, { simp [lt_irrefl] },
@@ -145,15 +147,15 @@ begin
     { exact h₀ _ (mem_insert_self _ _) } }
 end
 
-lemma convex.sum_mem (hs : convex ℝ s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1)
+lemma convex.sum_mem (hs : convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1)
   (hz : ∀ i ∈ t, z i ∈ s) :
   ∑ i in t, w i • z i ∈ s :=
 by simpa only [h₁, center_mass, inv_one, one_smul] using
   hs.center_mass_mem h₀ (h₁.symm ▸ zero_lt_one) hz
 
 lemma convex_iff_sum_mem :
-  convex ℝ s ↔
-    (∀ (t : finset E) (w : E → ℝ),
+  convex R s ↔
+    (∀ (t : finset E) (w : E → R),
       (∀ i ∈ t, 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x in t, w x • x ∈ s ) :=
 begin
   refine ⟨λ hs t w hw₀ hw₁ hts, hs.sum_mem hw₀ hw₁ hts, _⟩,
@@ -169,17 +171,17 @@ begin
       cases hi; subst i; simp [hx, hy, if_neg h_cases] } }
 end
 
-lemma finset.center_mass_mem_convex_hull (t : finset ι) {w : ι → ℝ} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
+lemma finset.center_mass_mem_convex_hull (t : finset ι) {w : ι → R} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
   (hws : 0 < ∑ i in t, w i) {z : ι → E} (hz : ∀ i ∈ t, z i ∈ s) :
-  t.center_mass w z ∈ convex_hull ℝ s :=
-(convex_convex_hull ℝ s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull ℝ s $ hz i hi)
+  t.center_mass w z ∈ convex_hull R s :=
+(convex_convex_hull R s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull R s $ hz i hi)
 
 -- TODO : Do we need other versions of the next lemma?
 
 /-- Convex hull of `s` is equal to the set of all centers of masses of `finset`s `t`, `z '' t ⊆ s`.
 This version allows finsets in any type in any universe. -/
 lemma convex_hull_eq (s : set E) :
-  convex_hull ℝ s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → ℝ) (z : ι → E)
+  convex_hull R s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → R) (z : ι → E)
     (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s),
     t.center_mass w z = x} :=
 begin
@@ -206,7 +208,7 @@ begin
 end
 
 lemma finset.convex_hull_eq (s : finset E) :
-  convex_hull ℝ ↑s = {x : E | ∃ (w : E → ℝ) (hw₀ : ∀ y ∈ s, 0 ≤ w y) (hw₁ : ∑ y in s, w y = 1),
+  convex_hull R ↑s = {x : E | ∃ (w : E → R) (hw₀ : ∀ y ∈ s, 0 ≤ w y) (hw₁ : ∑ y in s, w y = 1),
     s.center_mass w id = x} :=
 begin
   refine subset.antisymm (convex_hull_min _ _) _,
@@ -228,14 +230,14 @@ begin
 end
 
 lemma set.finite.convex_hull_eq {s : set E} (hs : finite s) :
-  convex_hull ℝ s = {x : E | ∃ (w : E → ℝ) (hw₀ : ∀ y ∈ s, 0 ≤ w y)
+  convex_hull R s = {x : E | ∃ (w : E → R) (hw₀ : ∀ y ∈ s, 0 ≤ w y)
     (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x} :=
 by simpa only [set.finite.coe_to_finset, set.finite.mem_to_finset, exists_prop]
   using hs.to_finset.convex_hull_eq
 
 /-- A weak version of Carathéodory's theorem. -/
 lemma convex_hull_eq_union_convex_hull_finite_subsets (s : set E) :
-  convex_hull ℝ s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull ℝ ↑t :=
+  convex_hull R s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull R ↑t :=
 begin
   refine subset.antisymm _ _,
   { rw convex_hull_eq,
@@ -252,15 +254,15 @@ end
 
 /-! ### `std_simplex` -/
 
-variables (ι) [fintype ι] {f : ι → ℝ}
+variables (ι) [fintype ι] {f : ι → R}
 
 /-- `std_simplex ι` is the convex hull of the canonical basis in `ι → ℝ`. -/
 lemma convex_hull_basis_eq_std_simplex :
-  convex_hull ℝ (range $ λ(i j:ι), if i = j then (1:ℝ) else 0) = std_simplex ι :=
+  convex_hull R (range $ λ(i j:ι), if i = j then (1:R) else 0) = std_simplex ι R :=
 begin
-  refine subset.antisymm (convex_hull_min _ (convex_std_simplex ι)) _,
+  refine subset.antisymm (convex_hull_min _ (convex_std_simplex ι R)) _,
   { rintros _ ⟨i, rfl⟩,
-    exact ite_eq_mem_std_simplex i },
+    exact ite_eq_mem_std_simplex R i },
   { rintros w ⟨hw₀, hw₁⟩,
     rw [pi_eq_sum_univ w, ← finset.univ.center_mass_eq_of_sum_1 _ hw₁],
     exact finset.univ.center_mass_mem_convex_hull (λ i hi, hw₀ i)
@@ -276,8 +278,8 @@ Since we have no sums over finite sets, we use sum over `@finset.univ _ hs.finty
 The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so that later we will not need
 to prove that this map is linear. -/
 lemma set.finite.convex_hull_eq_image {s : set E} (hs : finite s) :
-  convex_hull ℝ s = by haveI := hs.fintype; exact
-    (⇑(∑ x : s, (@linear_map.proj ℝ s _ (λ i, ℝ) _ _ x).smul_right x.1)) '' (std_simplex s) :=
+  convex_hull R s = by haveI := hs.fintype; exact
+    (⇑(∑ x : s, (@linear_map.proj R s _ (λ i, R) _ _ x).smul_right x.1)) '' (std_simplex s R) :=
 begin
   rw [← convex_hull_basis_eq_std_simplex, ← linear_map.convex_hull_image, ← set.range_comp, (∘)],
   apply congr_arg,
@@ -287,6 +289,6 @@ begin
 end
 
 /-- All values of a function `f ∈ std_simplex ι` belong to `[0, 1]`. -/
-lemma mem_Icc_of_mem_std_simplex (hf : f ∈ std_simplex ι) (x) :
-  f x ∈ Icc (0 : ℝ) 1 :=
+lemma mem_Icc_of_mem_std_simplex (hf : f ∈ std_simplex ι R) (x) :
+  f x ∈ Icc (0 : R) 1 :=
 ⟨hf.1 x, hf.2 ▸ finset.single_le_sum (λ y hy, hf.1 y) (finset.mem_univ x)⟩

src/analysis/convex/complex.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2019 Yury Kudriashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudriashov, Yaël Dillies
+-/
+import analysis.convex.basic
+import data.complex.module
+
+/-!
+# Convexity of half spaces in ℂ
+
+The open and closed half-spaces in ℂ given by an inequality on either the real or imaginary part
+are all convex over ℝ.
+-/
+
+lemma convex_halfspace_re_lt (r : ℝ) : convex ℝ {c : ℂ | c.re < r} :=
+convex_halfspace_lt (is_linear_map.mk complex.add_re complex.smul_re) _
+
+lemma convex_halfspace_re_le (r : ℝ) : convex ℝ {c : ℂ | c.re ≤ r} :=
+convex_halfspace_le (is_linear_map.mk complex.add_re complex.smul_re) _
+
+lemma convex_halfspace_re_gt (r : ℝ) : convex ℝ {c : ℂ | r < c.re } :=
+convex_halfspace_gt (is_linear_map.mk complex.add_re complex.smul_re) _
+
+lemma convex_halfspace_re_ge (r : ℝ) : convex ℝ {c : ℂ | r ≤ c.re} :=
+convex_halfspace_ge (is_linear_map.mk complex.add_re complex.smul_re) _
+
+lemma convex_halfspace_im_lt (r : ℝ) : convex ℝ {c : ℂ | c.im < r} :=
+convex_halfspace_lt (is_linear_map.mk complex.add_im complex.smul_im) _
+
+lemma convex_halfspace_im_le (r : ℝ) : convex ℝ {c : ℂ | c.im ≤ r} :=
+convex_halfspace_le (is_linear_map.mk complex.add_im complex.smul_im) _
+
+lemma convex_halfspace_im_gt (r : ℝ) : convex ℝ {c : ℂ | r < c.im} :=
+convex_halfspace_gt (is_linear_map.mk complex.add_im complex.smul_im) _
+
+lemma convex_halfspace_im_ge (r : ℝ) : convex ℝ {c : ℂ | r ≤ c.im} :=
+convex_halfspace_ge (is_linear_map.mk complex.add_im complex.smul_im) _

src/analysis/convex/extrema.lean

@@ -6,6 +6,7 @@ Authors: Frédéric Dupuis
 import analysis.convex.function
 import topology.algebra.affine
 import topology.local_extr
+import topology.instances.real
 
 /-!
 # Minima and maxima of convex functions

src/analysis/convex/extreme.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import analysis.convex.basic
+import data.real.basic
 
 /-!
 # Extreme sets

src/analysis/convex/function.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, François Dupuis
 -/
 import analysis.convex.combination
+import data.real.basic
+import algebra.module.ordered
 
 /-!
 # Convex and concave functions

src/analysis/convex/topology.lean

@@ -44,7 +44,7 @@ variables [fintype ι]
 
 /-- Every vector in `std_simplex ι` has `max`-norm at most `1`. -/
 lemma std_simplex_subset_closed_ball :
-  std_simplex ι ⊆ metric.closed_ball 0 1 :=
+  std_simplex ι ℝ ⊆ metric.closed_ball 0 1 :=
 begin
   assume f hf,
   rw [metric.mem_closed_ball, dist_zero_right],
@@ -57,17 +57,17 @@ end
 variable (ι)
 
 /-- `std_simplex ι` is bounded. -/
-lemma bounded_std_simplex : metric.bounded (std_simplex ι) :=
+lemma bounded_std_simplex : metric.bounded (std_simplex ι ℝ) :=
 (metric.bounded_iff_subset_ball 0).2 ⟨1, std_simplex_subset_closed_ball⟩
 
 /-- `std_simplex ι` is closed. -/
-lemma is_closed_std_simplex : is_closed (std_simplex ι) :=
-(std_simplex_eq_inter ι).symm ▸ is_closed.inter
+lemma is_closed_std_simplex : is_closed (std_simplex ι ℝ) :=
+(std_simplex_eq_inter ι ℝ).symm ▸ is_closed.inter
   (is_closed_Inter $ λ i, is_closed_le continuous_const (continuous_apply i))
   (is_closed_eq (continuous_finset_sum _ $ λ x _, continuous_apply x) continuous_const)
 
 /-- `std_simplex ι` is compact. -/
-lemma compact_std_simplex : is_compact (std_simplex ι) :=
+lemma compact_std_simplex : is_compact (std_simplex ι ℝ) :=
 metric.compact_iff_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩
 
 end std_simplex