From 598ac18969ed9b131060327d2213d4fc96b0f6ef Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Fri, 17 Sep 2021 20:59:35 +0200 Subject: [PATCH 01/17] initial commit --- src/analysis/convex/combination.lean | 72 ++++++++++++++-------------- 1 file changed, 36 insertions(+), 36 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 7ab43de5178c7..8eca503e06552 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -25,44 +25,44 @@ 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] - {s : set E} +variables {𝕜 E ι ι' : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 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 := -(∑ i in t, w i)⁻¹ • (∑ i in t, w i • z i) +def linear_combination (p : ι → E) : + (ι →₀ 𝕜) →ₗ[𝕜] E := +⟨λ w : ι →₀ 𝕜, w.sum (λ i _, w i • p i), sorry⟩ -variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι → ℝ) (z : ι → E) +variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι →₀ 𝕜) (p : ι → E) open finset -lemma finset.center_mass_empty : (∅ : finset ι).center_mass w z = 0 := -by simp only [center_mass, sum_empty, smul_zero] +lemma linear_combination_zero : linear_combination p (0 : ι →₀ 𝕜) = 0 := +by rw [linear_combination, linear_map.map_zero] lemma finset.center_mass_pair (hne : i ≠ j) : - ({i, j} : finset ι).center_mass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j := + ({i, j} : finset ι).center_mass w p = (w i / (w i + w j)) • p i + (w j / (w i + w j)) • p j := by simp only [center_mass, sum_pair hne, smul_add, (mul_smul _ _ _).symm, div_eq_inv_mul] variable {w} lemma finset.center_mass_insert (ha : i ∉ t) (hw : ∑ j in t, w j ≠ 0) : - (insert i t).center_mass w z = (w i / (w i + ∑ j in t, w j)) • z i + - ((∑ j in t, w j) / (w i + ∑ j in t, w j)) • t.center_mass w z := + (insert i t).center_mass w p = (w i / (w i + ∑ j in t, w j)) • p i + + ((∑ j in t, w j) / (w i + ∑ j in t, w j)) • t.center_mass w p := begin simp only [center_mass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul], congr' 2, rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div] end -lemma finset.center_mass_singleton (hw : w i ≠ 0) : ({i} : finset ι).center_mass w z = z i := +lemma finset.center_mass_singleton (hw : w i ≠ 0) : ({i} : finset ι).center_mass w p = p i := by rw [center_mass, sum_singleton, sum_singleton, ← mul_smul, inv_mul_cancel hw, one_smul] lemma finset.center_mass_eq_of_sum_1 (hw : ∑ i in t, w i = 1) : - t.center_mass w z = ∑ i in t, w i • z i := + t.center_mass w p = ∑ i in t, w i • p i := by simp only [finset.center_mass, hw, inv_one, one_smul] -lemma finset.center_mass_smul : t.center_mass w (λ i, c • z i) = c • t.center_mass w z := +lemma finset.center_mass_smul : t.center_mass w (λ i, c • p i) = c • t.center_mass w p := by simp only [finset.center_mass, finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc] /-- A convex combination of two centers of mass is a center of mass as well. This version @@ -84,19 +84,19 @@ 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) + (s : finset ι) (w₁ w₂ : ι → ℝ) (p : ι → E) (hw₁ : ∑ i in s, w₁ i = 1) (hw₂ : ∑ i in s, w₂ i = 1) (a b : ℝ) (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 := + a • s.center_mass w₁ p + b • s.center_mass w₂ p = + s.center_mass (λ i, a * w₁ i + b * w₂ i) p := 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 else 0) p = p i := begin rw [finset.center_mass_eq_of_sum_1], - transitivity ∑ j in t, if (i = j) then z i else 0, + transitivity ∑ j in t, if (i = j) then p i else 0, { congr' with i, split_ifs, exacts [h ▸ one_smul _ _, zero_smul _ _] }, { rw [sum_ite_eq, if_pos hi] }, { rw [sum_ite_eq, if_pos hi] } @@ -106,7 +106,7 @@ variables {t w} lemma finset.center_mass_subset {t' : finset ι} (ht : t ⊆ t') (h : ∀ i ∈ t', i ∉ t → w i = 0) : - t.center_mass w z = t'.center_mass w z := + t.center_mass w p = t'.center_mass w p := begin rw [center_mass, sum_subset ht h, smul_sum, center_mass, smul_sum], apply sum_subset ht, @@ -115,8 +115,8 @@ begin end lemma finset.center_mass_filter_ne_zero : - (t.filter (λ i, w i ≠ 0)).center_mass w z = t.center_mass w z := -finset.center_mass_subset z (filter_subset _ _) $ λ i hit hit', + (t.filter (λ i, w i ≠ 0)).center_mass w p = t.center_mass w p := +finset.center_mass_subset p (filter_subset _ _) $ λ i hit hit', by simpa only [hit, mem_filter, true_and, ne.def, not_not] using hit' variable {z} @@ -124,16 +124,16 @@ 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) : - (∀ i ∈ t, 0 ≤ w i) → (0 < ∑ i in t, w i) → (∀ i ∈ t, z i ∈ s) → t.center_mass w z ∈ s := + (∀ i ∈ t, 0 ≤ w i) → (0 < ∑ i in t, w i) → (∀ i ∈ t, p i ∈ s) → t.center_mass w p ∈ s := begin induction t using finset.induction with i t hi ht, { simp [lt_irrefl] }, intros h₀ hpos hmem, - have zi : z i ∈ s, from hmem _ (mem_insert_self _ _), + have zi : p i ∈ s, from hmem _ (mem_insert_self _ _), have hs₀ : ∀ j ∈ t, 0 ≤ w j, from λ j hj, h₀ j $ mem_insert_of_mem hj, rw [sum_insert hi] at hpos, by_cases hsum_t : ∑ j in t, w j = 0, { have ws : ∀ j ∈ t, w j = 0, from (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t, - have wz : ∑ j in t, w j • z j = 0, from sum_eq_zero (λ i hi, by simp [ws i hi]), + have wp : ∑ j in t, w j • p j = 0, from sum_eq_zero (λ i hi, by simp [ws i hi]), simp only [center_mass, sum_insert hi, wz, hsum_t, add_zero], simp only [hsum_t, add_zero] at hpos, rw [← mul_smul, inv_mul_cancel (ne_of_gt hpos), one_smul], @@ -146,8 +146,8 @@ begin end lemma convex.sum_mem (hs : convex ℝ 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 := + (hp : ∀ i ∈ t, p i ∈ s) : + ∑ i in t, w i • p i ∈ s := by simpa only [h₁, center_mass, inv_one, one_smul] using hs.center_mass_mem h₀ (h₁.symm ▸ zero_lt_one) hz @@ -160,7 +160,7 @@ begin intros h x y hx hy a b ha hb hab, by_cases h_cases: x = y, { rw [h_cases, ←add_smul, hab, one_smul], exact hy }, - { convert h {x, y} (λ z, if z = y then b else a) _ _ _, + { convert h {x, y} (λ z, if p = y then b else a) _ _ _, { simp only [sum_pair h_cases, if_neg h_cases, if_pos rfl] }, { simp_intros i hi, cases hi; subst i; simp [ha, hb, if_neg h_cases] }, @@ -170,18 +170,18 @@ begin end lemma finset.center_mass_mem_convex_hull (t : finset ι) {w : ι → ℝ} (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) + (hws : 0 < ∑ i in t, w i) {p : ι → E} (hp : ∀ i ∈ t, p i ∈ s) : + t.center_mass w p ∈ convex_hull ℝ s := +(convex_convex_hull ℝ s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull ℝ s $ hp 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`. +/-- Convex hull of `s` is equal to the set of all centers of masses of `finset`s `t`, `p '' 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) - (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} := + convex_hull ℝ s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → ℝ) (p : ι → E) + (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hp : ∀ i ∈ t, p i ∈ s), + t.center_mass w p = x} := begin refine subset.antisymm (convex_hull_min _ _) _, { intros x hx, @@ -202,7 +202,7 @@ begin rw [finset.mem_union, finset.mem_map, finset.mem_map] at hi, rcases hi with ⟨j, hj, rfl⟩|⟨j, hj, rfl⟩; apply_rules [hzx, hzy] } }, { rintros _ ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩, - exact t.center_mass_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) hz } + exact t.center_mass_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) hp } end lemma finset.convex_hull_eq (s : finset E) : @@ -243,7 +243,7 @@ begin simp only [mem_Union], refine ⟨t.image z, _, _⟩, { rw [coe_image, set.image_subset_iff], - exact hz }, + exact hp }, { apply t.center_mass_mem_convex_hull hw₀, { simp only [hw₁, zero_lt_one] }, { exact λ i hi, finset.mem_coe.2 (finset.mem_image_of_mem _ hi) } } }, From 86ee2142dc0209c362f141c9b22f651c9ada68c9 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Fri, 17 Sep 2021 23:17:25 +0200 Subject: [PATCH 02/17] some more --- src/analysis/convex/combination.lean | 233 ++++++++++++++------------- 1 file changed, 119 insertions(+), 114 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 8eca503e06552..3c4fd73181de4 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -12,148 +12,153 @@ This file defines convex combinations of points in a vector space. ## Main declarations -* `finset.center_mass`: Center of mass of a finite family of points. +* `finset.linear_combination`: Center of mass of a finite family of points. ## Implementation notes -We divide by the sum of the weights in the definition of `finset.center_mass` because of the way +We divide by the sum of the weights in the definition of `finset.linear_combination` because of the way mathematical arguments go: one doesn't change weights, but merely adds some. This also makes a few lemmas unconditional on the sum of the weights being `1`. + +## TODO + +Change `finset.linear_combination : finset ι → (ι → E) → (ι → 𝕜) → E` to +`linear_combination : (ι → E) →ₗ[𝕜] (ι →₀ 𝕜) →ₗ[𝕜] E`. Same goes for `finset.affine_combination`. -/ open set open_locale big_operators classical -universes u u' -variables {𝕜 E ι ι' : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] +namespace finset -/-- Center of mass of a finite collection of points with prescribed weights. -Note that we require neither `0 ≤ w i` nor `∑ w = 1`. -/ -def linear_combination (p : ι → E) : - (ι →₀ 𝕜) →ₗ[𝕜] E := -⟨λ w : ι →₀ 𝕜, w.sum (λ i _, w i • p i), sorry⟩ +/-- Linear combination of a finite collection of points with prescribed weights. -/ +def linear_combination {𝕜 E ι : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] + (s : finset ι) (p : ι → E) (w : ι → 𝕜) : E := +∑ i in s, w i • p i -variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι →₀ 𝕜) (p : ι → E) +section ordered_semiring +variables {𝕜 E ι ι' : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] + (i j : ι) (c : 𝕜) (s : finset ι) (p : ι → E) (w : ι → 𝕜) -open finset +lemma linear_combination_def : + s.linear_combination p w = ∑ i in s, w i • p i := rfl -lemma linear_combination_zero : linear_combination p (0 : ι →₀ 𝕜) = 0 := -by rw [linear_combination, linear_map.map_zero] +lemma linear_combination_empty : (∅ : finset ι).linear_combination p w = 0 := +by simp only [linear_combination, sum_empty, smul_zero] -lemma finset.center_mass_pair (hne : i ≠ j) : - ({i, j} : finset ι).center_mass w p = (w i / (w i + w j)) • p i + (w j / (w i + w j)) • p j := -by simp only [center_mass, sum_pair hne, smul_add, (mul_smul _ _ _).symm, div_eq_inv_mul] +lemma linear_combination_pair (hne : i ≠ j) : + ({i, j} : finset ι).linear_combination p w = w i • p i + w j • p j := +by rw [linear_combination, sum_pair hne] variable {w} -lemma finset.center_mass_insert (ha : i ∉ t) (hw : ∑ j in t, w j ≠ 0) : - (insert i t).center_mass w p = (w i / (w i + ∑ j in t, w j)) • p i + - ((∑ j in t, w j) / (w i + ∑ j in t, w j)) • t.center_mass w p := -begin - simp only [center_mass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul], - congr' 2, - rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div] -end - -lemma finset.center_mass_singleton (hw : w i ≠ 0) : ({i} : finset ι).center_mass w p = p i := -by rw [center_mass, sum_singleton, sum_singleton, ← mul_smul, inv_mul_cancel hw, one_smul] - -lemma finset.center_mass_eq_of_sum_1 (hw : ∑ i in t, w i = 1) : - t.center_mass w p = ∑ i in t, w i • p i := -by simp only [finset.center_mass, hw, inv_one, one_smul] +lemma linear_combination_singleton : + ({i} : finset ι).linear_combination p w = w i • p i := +by rw [linear_combination, sum_singleton] -lemma finset.center_mass_smul : t.center_mass w (λ i, c • p i) = c • t.center_mass w p := -by simp only [finset.center_mass, finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc] +lemma linear_combination_insert (ha : i ∉ s) : + (insert i s).linear_combination p w = w i • p i + s.linear_combination p w := +by rw [linear_combination, linear_combination, sum_insert ha] /-- 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) : - 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)) - (sum.elim zs zt) := +lemma linear_combination_segment' (s : finset ι) (t : finset ι') (ws : ι → 𝕜) (ps : ι → E) + (wt : ι' → 𝕜) (pt : ι' → E) (a b : 𝕜) (hab : a + b = 1) : + a • s.linear_combination ps ws + b • t.linear_combination pt wt = + (s.map function.embedding.inl ∪ t.map function.embedding.inr).linear_combination + (sum.elim ps pt) + (sum.elim (λ i, a * ws i) (λ j, b * wt j)) := begin - rw [s.center_mass_eq_of_sum_1 _ hws, t.center_mass_eq_of_sum_1 _ hwt, - smul_sum, smul_sum, ← finset.sum_sum_elim, finset.center_mass_eq_of_sum_1], - { congr' with ⟨⟩; simp only [sum.elim_inl, sum.elim_inr, mul_smul] }, - { rw [sum_sum_elim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab] } + unfold linear_combination, + rw [smul_sum, smul_sum, ← sum_sum_elim], + { congr' with ⟨⟩; simp only [sum.elim_inl, sum.elim_inr, mul_smul] } 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₂ : ι → ℝ) (p : ι → E) - (hw₁ : ∑ i in s, w₁ i = 1) (hw₂ : ∑ i in s, w₂ i = 1) (a b : ℝ) (hab : a + b = 1) : - a • s.center_mass w₁ p + b • s.center_mass w₂ p = - s.center_mass (λ i, a * w₁ i + b * w₂ i) p := -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) p = p i := +lemma linear_combination_segment (s : finset ι) (w₁ w₂ : ι → 𝕜) (p : ι → E) (a b : 𝕜) + (hab : a + b = 1) : + a • s.linear_combination p w₁ + b • s.linear_combination p w₂ = + s.linear_combination p (λ i, a * w₁ i + b * w₂ i) := begin - rw [finset.center_mass_eq_of_sum_1], - transitivity ∑ j in t, if (i = j) then p i else 0, + unfold linear_combination, + simp only [linear_combination_def, smul_sum, sum_add_distrib, add_smul, mul_smul, *], +end + +lemma linear_combination_ite_eq (hi : i ∈ s) : + s.linear_combination p (λ j, if (i = j) then 1 else 0) = p i := +begin + rw linear_combination, + transitivity ∑ j in s, if (i = j) then p i else 0, { congr' with i, split_ifs, exacts [h ▸ one_smul _ _, zero_smul _ _] }, - { rw [sum_ite_eq, if_pos hi] }, { rw [sum_ite_eq, if_pos hi] } end -variables {t w} +variables {s w} -lemma finset.center_mass_subset {t' : finset ι} (ht : t ⊆ t') - (h : ∀ i ∈ t', i ∉ t → w i = 0) : - t.center_mass w p = t'.center_mass w p := +lemma linear_combination_subset {t : finset ι} (ht : s ⊆ t) + (h : ∀ i ∈ t, i ∉ s → w i = 0) : + s.linear_combination p w = t.linear_combination p w := begin - rw [center_mass, sum_subset ht h, smul_sum, center_mass, smul_sum], - apply sum_subset ht, - assume i hit' hit, - rw [h i hit' hit, zero_smul, smul_zero] + rw [linear_combination, linear_combination], + exact sum_subset ht (λ i hit his, by rw [h i hit his, zero_smul]), end -lemma finset.center_mass_filter_ne_zero : - (t.filter (λ i, w i ≠ 0)).center_mass w p = t.center_mass w p := -finset.center_mass_subset p (filter_subset _ _) $ λ i hit hit', +lemma linear_combination_filter_ne_zero : + (s.filter (λ i, w i ≠ 0)).linear_combination p w = s.linear_combination p w := +linear_combination_subset p (filter_subset _ _) $ λ i hit hit', by simpa only [hit, mem_filter, true_and, ne.def, not_not] using hit' -variable {z} +variables {p} {t : set E} + +end ordered_semiring + +section ordered_comm_semiring +variables {𝕜 E ι ι' : Type*} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] + (c : 𝕜) (s : finset ι) (p : ι → E) {w : ι → 𝕜} + +lemma linear_combination_smul : + s.linear_combination (λ i, c • p i) w = c • s.linear_combination p w := +by simp_rw [linear_combination, smul_sum, smul_comm c] + +end ordered_comm_semiring + +section linear_ordered_field +variables {𝕜 E ι ι' : Type*} [linear_ordered_field 𝕜] [add_comm_monoid E] [module 𝕜 E] + {s : set E} {t : finset ι} {p : ι → E} {w : ι → 𝕜} /-- 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) : - (∀ i ∈ t, 0 ≤ w i) → (0 < ∑ i in t, w i) → (∀ i ∈ t, p i ∈ s) → t.center_mass w p ∈ s := +lemma convex.linear_combination_mem (ht : convex 𝕜 s) : + (∀ i ∈ t, 0 ≤ w i) → (∑ i in t, w i = 1) → (∀ i ∈ t, p i ∈ s) → t.linear_combination p w ∈ s := begin induction t using finset.induction with i t hi ht, { simp [lt_irrefl] }, - intros h₀ hpos hmem, + intros h₀ h₁ hmem, have zi : p i ∈ s, from hmem _ (mem_insert_self _ _), have hs₀ : ∀ j ∈ t, 0 ≤ w j, from λ j hj, h₀ j $ mem_insert_of_mem hj, - rw [sum_insert hi] at hpos, + rw [sum_insert hi] at h₁, + rw linear_combination_insert _ _ _ hi, by_cases hsum_t : ∑ j in t, w j = 0, - { have ws : ∀ j ∈ t, w j = 0, from (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t, - have wp : ∑ j in t, w j • p j = 0, from sum_eq_zero (λ i hi, by simp [ws i hi]), - simp only [center_mass, sum_insert hi, wz, hsum_t, add_zero], - simp only [hsum_t, add_zero] at hpos, - rw [← mul_smul, inv_mul_cancel (ne_of_gt hpos), one_smul], + { have wt : ∀ j ∈ t, w j = 0, from (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t, + have wp : t.linear_combination p w = 0, from sum_eq_zero (λ i hi, by simp [wt i hi]), + rw [hsum_t, add_zero] at h₁, + rw [wp, add_zero, h₁, one_smul], exact zi }, - { rw [finset.center_mass_insert _ _ _ hi hsum_t], - refine convex_iff_div.1 hs zi (ht hs₀ _ _) _ (sum_nonneg hs₀) hpos, + { refine convex_iff_div.1 hs zi (ht hs₀ _ _) _ (sum_nonneg hs₀) h₁, { exact lt_of_le_of_ne (sum_nonneg hs₀) (ne.symm hsum_t) }, { intros j hj, exact hmem j (mem_insert_of_mem hj) }, { 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 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hp : ∀ i ∈ t, p i ∈ s) : ∑ i in t, w i • p i ∈ s := -by simpa only [h₁, center_mass, inv_one, one_smul] using - hs.center_mass_mem h₀ (h₁.symm ▸ zero_lt_one) hz +by simpa only [h₁, linear_combination, inv_one, one_smul] using + hs.linear_combination_mem h₀ (h₁.symm ▸ zero_lt_one) hz lemma convex_iff_sum_mem : - convex ℝ s ↔ - (∀ (t : finset E) (w : E → ℝ), + convex 𝕜 s ↔ + (∀ (t : finset E) (w : E → 𝕜), (∀ 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,28 +174,28 @@ 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) - (hws : 0 < ∑ i in t, w i) {p : ι → E} (hp : ∀ i ∈ t, p i ∈ s) : - t.center_mass w p ∈ convex_hull ℝ s := -(convex_convex_hull ℝ s).center_mass_mem hw₀ hws (λ i hi, subset_convex_hull ℝ s $ hp i hi) +lemma finset.linear_combination_mem_convex_hull (t : finset ι) {w : ι → 𝕜} (hw₀ : ∀ i ∈ t, 0 ≤ w i) + (hws : ∑ i in t, w i = 1) {p : ι → E} (hp : ∀ i ∈ t, p i ∈ s) : + s.linear_combination p w ∈ convex_hull 𝕜 s := +(convex_convex_hull 𝕜 s).linear_combination_mem hw₀ hws (λ i hi, subset_convex_hull 𝕜 s $ hp 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`, `p '' 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 : ι → ℝ) (p : ι → E) + convex_hull 𝕜 s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → 𝕜) (p : ι → E) (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hp : ∀ i ∈ t, p i ∈ s), - t.center_mass w p = x} := + s.linear_combination p w = x} := begin refine subset.antisymm (convex_hull_min _ _) _, { intros x hx, use [punit, {punit.star}, λ _, 1, λ _, x, λ _ _, zero_le_one, finset.sum_singleton, λ _ _, hx], - simp only [finset.center_mass, finset.sum_singleton, inv_one, one_smul] }, + simp only [finset.linear_combination, finset.sum_singleton, inv_one, one_smul] }, { rintros x y ⟨ι, sx, wx, zx, hwx₀, hwx₁, hzx, rfl⟩ ⟨ι', sy, wy, zy, hwy₀, hwy₁, hzy, rfl⟩ a b ha hb hab, - rw [finset.center_mass_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab], + rw [finset.linear_combination_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab], refine ⟨_, _, _, _, _, _, _, rfl⟩, { rintros i hi, rw [finset.mem_union, finset.mem_map, finset.mem_map] at hi, @@ -202,40 +207,40 @@ begin rw [finset.mem_union, finset.mem_map, finset.mem_map] at hi, rcases hi with ⟨j, hj, rfl⟩|⟨j, hj, rfl⟩; apply_rules [hzx, hzy] } }, { rintros _ ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩, - exact t.center_mass_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) hp } + exact s.linear_combination_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) hp } 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), - s.center_mass w id = x} := + convex_hull 𝕜 ↑s = {x : E | ∃ (w : E → 𝕜) (hw₀ : ∀ y ∈ s, 0 ≤ w y) (hw₁ : ∑ y in s, w y = 1), + s.linear_combination w id = x} := begin refine subset.antisymm (convex_hull_min _ _) _, { intros x hx, rw [finset.mem_coe] at hx, - refine ⟨_, _, _, finset.center_mass_ite_eq _ _ _ hx⟩, + refine ⟨_, _, _, finset.linear_combination_ite_eq _ _ _ hx⟩, { intros, split_ifs, exacts [zero_le_one, le_refl 0] }, { rw [finset.sum_ite_eq, if_pos hx] } }, { rintros x y ⟨wx, hwx₀, hwx₁, rfl⟩ ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab, - rw [finset.center_mass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab], + rw [finset.linear_combination_segment _ _ _ _ hwx₁ hwy₁ _ _ hab], refine ⟨_, _, _, rfl⟩, { rintros i hi, apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀], }, { simp only [finset.sum_add_distrib, finset.mul_sum.symm, mul_one, *] } }, { rintros _ ⟨w, hw₀, hw₁, rfl⟩, - exact s.center_mass_mem_convex_hull (λ x hx, hw₀ _ hx) + exact s.linear_combination_mem_convex_hull (λ x hx, hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) (λ x hx, hx) } 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) - (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x} := + convex_hull 𝕜 s = {x : E | ∃ (w : E → 𝕜) (hw₀ : ∀ y ∈ s, 0 ≤ w y) + (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.linear_combination 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 𝕜 s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull 𝕜 ↑t := begin refine subset.antisymm _ _, { rw convex_hull_eq, @@ -244,7 +249,7 @@ begin refine ⟨t.image z, _, _⟩, { rw [coe_image, set.image_subset_iff], exact hp }, - { apply t.center_mass_mem_convex_hull hw₀, + { apply s.linear_combination_mem_convex_hull hw₀, { simp only [hw₁, zero_lt_one] }, { exact λ i hi, finset.mem_coe.2 (finset.mem_image_of_mem _ hi) } } }, { exact Union_subset (λ i, Union_subset convex_hull_mono), }, @@ -252,32 +257,32 @@ end /-! ### `std_simplex` -/ -variables (ι) [fintype ι] {f : ι → ℝ} +variables (ι) [fintype ι] {f : ι → 𝕜} -/-- `std_simplex ι` is the convex hull of the canonical basis in `ι → ℝ`. -/ +/-- `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 𝕜 (range $ λ(i j:ι), if i = j then (1:𝕜) else 0) = std_simplex ι := begin refine subset.antisymm (convex_hull_min _ (convex_std_simplex ι)) _, { rintros _ ⟨i, rfl⟩, exact ite_eq_mem_std_simplex 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) + rw [pi_eq_sum_univ w, ← finset.univ.linear_combination_eq_of_sum_1 _ hw₁], + exact finset.univ.linear_combination_mem_convex_hull (λ i hi, hw₀ i) (hw₁.symm ▸ zero_lt_one) (λ i hi, mem_range_self i) } end variable {ι} -/-- The convex hull of a finite set is the image of the standard simplex in `s → ℝ` +/-- The convex hull of a finite set is the image of the standard simplex in `s → 𝕜` under the linear map sending each function `w` to `∑ x in s, w x • x`. Since we have no sums over finite sets, we use sum over `@finset.univ _ hs.fintype`. -The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so that later we will not need +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 𝕜 s = by haveI := hs.fintype; exact + (⇑(∑ x : s, (@linear_map.proj 𝕜 s _ (λ i, 𝕜) _ _ x).smul_right x.1)) '' (std_simplex s) := begin rw [← convex_hull_basis_eq_std_simplex, ← linear_map.convex_hull_image, ← set.range_comp, (∘)], apply congr_arg, @@ -288,5 +293,5 @@ 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 := + f x ∈ Icc (0 : 𝕜) 1 := ⟨hf.1 x, hf.2 ▸ finset.single_le_sum (λ y hy, hf.1 y) (finset.mem_univ x)⟩ From 67ba2fa8e305b5e85501981302d461ab4760032f Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Sat, 18 Sep 2021 11:03:52 +0200 Subject: [PATCH 03/17] generalize std_simplex --- src/analysis/convex/basic.lean | 19 +-- src/analysis/convex/caratheodory.lean | 8 +- src/analysis/convex/combination.lean | 166 +++++++++++++++----------- src/analysis/convex/function.lean | 76 ++++++------ src/analysis/convex/independent.lean | 2 +- src/analysis/convex/integral.lean | 16 +-- src/analysis/convex/topology.lean | 18 +-- 7 files changed, 164 insertions(+), 141 deletions(-) diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean index 262e75d603907..cc0923ae048f4 100644 --- a/src/analysis/convex/basic.lean +++ b/src/analysis/convex/basic.lean @@ -18,7 +18,7 @@ In a 𝕜-vector space, we define the following objects and properties. * `convex_hull 𝕜 s`: The minimal convex set that includes `s`. In order theory speak, this is a closure operator. * Standard simplex `std_simplex ι [fintype ι]` is the intersection of the positive quadrant with - the hyperplane `s.sum = 1` in the space `ι → ℝ`. + the hyperplane `s.sum = 1` in the space `ι → 𝕜`. We also provide various equivalent versions of the definitions above, prove that some specific sets are convex. @@ -1056,24 +1056,25 @@ end ordered_ring end convex_hull -variables {ι ι' : Type*} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] {s : set E} +variables {ι ι' : Type*} [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} /-! ### Simplex -/ section simplex -variables (ι) [fintype ι] {f : ι → ℝ} +variables (ι) [fintype ι] {f : ι → 𝕜} -/-- 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 (ι → ℝ) := +/-- The standard simplex in the space of finitely supported functions `ι →₀ 𝕜` is the set +of vectors with non-negative coordinates with total sum `1`. This is the free object in the category +of convex spaces.-/ +def std_simplex : set (ι → 𝕜) := {f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1} lemma std_simplex_eq_inter : - std_simplex ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1} := + std_simplex 𝕜 ι = (⋂ 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 𝕜 (std_simplex 𝕜 ι) := begin refine λ f g hf hg a b ha hb hab, ⟨λ x, _, _⟩, { apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1] }, @@ -1084,7 +1085,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:𝕜) 0) ∈ std_simplex 𝕜 ι := ⟨λ j, by simp only; split_ifs; norm_num, by rw [finset.sum_ite_eq, if_pos (finset.mem_univ _)]⟩ end simplex diff --git a/src/analysis/convex/caratheodory.lean b/src/analysis/convex/caratheodory.lean index c5159e37c09c3..7f1da0be75e7d 100644 --- a/src/analysis/convex/caratheodory.lean +++ b/src/analysis/convex/caratheodory.lean @@ -80,12 +80,12 @@ begin ... ≤ f e : fpos e het, { apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg) }, { simpa only [mem_filter, het, true_and, not_lt] using hes } } }, - { simp only [subtype.coe_mk, center_mass_eq_of_sum_1 _ id ksum, id], + { simp only [subtype.coe_mk, id], calc ∑ e in t.erase i₀, k e • e = ∑ e in t, k e • e : sum_erase _ (by rw [hk, zero_smul]) ... = ∑ e in t, (f e - f i₀ / g i₀ * g e) • e : rfl - ... = t.center_mass f id : _, + ... = t.linear_combination id f : _, simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, - sub_zero, center_mass, fsum, inv_one, one_smul, id.def] } + sub_zero, linear_combination, fsum, inv_one, one_smul, id.def] } end variables {s : set E} {x : E} (hx : x ∈ convex_hull ℝ s) @@ -176,6 +176,6 @@ begin { erw [finset.sum_attach, finset.sum_filter_ne_zero, hw₂] }, { change ∑ (i : t') in t'.attach, (λ e, w e • e) ↑i = x, erw [finset.sum_attach, finset.sum_filter_of_ne], - { rw t.center_mass_eq_of_sum_1 id hw₂ at hw₃, exact hw₃ }, + { exact hw₃ }, { intros e he hwe contra, apply hwe, rw [contra, zero_smul] } } end diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 3c4fd73181de4..b4f9a28adca49 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -6,24 +6,23 @@ Authors: Yury Kudriashov import analysis.convex.basic /-! -# Convex combinations +# Linear combinations -This file defines convex combinations of points in a vector space. +This file defines linear combinations of points in a semimodule and proves results about convex +combinations. Convex combinations in a semimodule can be modelled as linear combinations with +nonnegative coefficients summing to `1`. In an affine space, they can be modelled through affine combinations. ## Main declarations * `finset.linear_combination`: Center of mass of a finite family of points. -## Implementation notes - -We divide by the sum of the weights in the definition of `finset.linear_combination` because of the way -mathematical arguments go: one doesn't change weights, but merely adds some. This also makes a few -lemmas unconditional on the sum of the weights being `1`. - ## TODO Change `finset.linear_combination : finset ι → (ι → E) → (ι → 𝕜) → E` to `linear_combination : (ι → E) →ₗ[𝕜] (ι →₀ 𝕜) →ₗ[𝕜] E`. Same goes for `finset.affine_combination`. + +Ultimately, this file should be about `convex_combination`, which will generalize both +`affine_combination` and `linear_combination`. The latter should find a home in `linear_algebra`. -/ open set @@ -60,6 +59,10 @@ lemma linear_combination_insert (ha : i ∉ s) : (insert i s).linear_combination p w = w i • p i + s.linear_combination p w := by rw [linear_combination, linear_combination, sum_insert ha] +lemma linear_combination_const_left (x : E) : + s.linear_combination (λ _, x) w = (∑ i in s, w i) • x := +by rw [linear_combination, finset.sum_smul] + /-- A convex combination of two centers of mass is a center of mass as well. This version deals with two different index types. -/ lemma linear_combination_segment' (s : finset ι) (t : finset ι') (ws : ι → 𝕜) (ps : ι → E) @@ -86,7 +89,7 @@ begin end lemma linear_combination_ite_eq (hi : i ∈ s) : - s.linear_combination p (λ j, if (i = j) then 1 else 0) = p i := + s.linear_combination p (λ j, if (i = j) then (1 : 𝕜) else 0) = p i := begin rw linear_combination, transitivity ∑ j in s, if (i = j) then p i else 0, @@ -94,6 +97,10 @@ begin { rw [sum_ite_eq, if_pos hi] } end +lemma linear_combination_smul_right : + s.linear_combination p (c • w) = c • s.linear_combination p w := +by simp_rw [linear_combination, smul_sum, pi.smul_apply, smul_assoc] + variables {s w} lemma linear_combination_subset {t : finset ι} (ht : s ⊆ t) @@ -117,9 +124,9 @@ section ordered_comm_semiring variables {𝕜 E ι ι' : Type*} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (c : 𝕜) (s : finset ι) (p : ι → E) {w : ι → 𝕜} -lemma linear_combination_smul : - s.linear_combination (λ i, c • p i) w = c • s.linear_combination p w := -by simp_rw [linear_combination, smul_sum, smul_comm c] +lemma linear_combination_smul_left : + s.linear_combination (c • p) w = c • s.linear_combination p w := +by simp_rw [linear_combination, smul_sum, pi.smul_apply, smul_comm c] end ordered_comm_semiring @@ -127,45 +134,52 @@ section linear_ordered_field variables {𝕜 E ι ι' : Type*} [linear_ordered_field 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} {t : finset ι} {p : ι → E} {w : ι → 𝕜} -/-- 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.linear_combination_mem (ht : convex 𝕜 s) : +lemma linear_combination_normalize (hw : ∑ i in t, w i ≠ 0) : + t.linear_combination p w = (∑ i in t, w i) • t.linear_combination p ((∑ i in t, w i)⁻¹ • w) := +by rw [linear_combination_smul_right, smul_inv_smul' hw] + +/-- The linear combination of a finite subset of a convex set belongs to the set +provided that all weights are non-negative, and the total weight is `1`. -/ +lemma _root_.convex.linear_combination_mem (hs : convex 𝕜 s) : (∀ i ∈ t, 0 ≤ w i) → (∑ i in t, w i = 1) → (∀ i ∈ t, p i ∈ s) → t.linear_combination p w ∈ s := begin - induction t using finset.induction with i t hi ht, { simp [lt_irrefl] }, + induction t using finset.induction with i t hi ht generalizing w, { simp [lt_irrefl] }, intros h₀ h₁ hmem, - have zi : p i ∈ s, from hmem _ (mem_insert_self _ _), - have hs₀ : ∀ j ∈ t, 0 ≤ w j, from λ j hj, h₀ j $ mem_insert_of_mem hj, + have hpi : p i ∈ s, from hmem _ (mem_insert_self _ _), + have ht₀ : ∀ j ∈ t, 0 ≤ w j, from λ j hj, h₀ j $ mem_insert_of_mem hj, rw [sum_insert hi] at h₁, rw linear_combination_insert _ _ _ hi, by_cases hsum_t : ∑ j in t, w j = 0, - { have wt : ∀ j ∈ t, w j = 0, from (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t, + { have wt : ∀ j ∈ t, w j = 0, from (sum_eq_zero_iff_of_nonneg ht₀).1 hsum_t, have wp : t.linear_combination p w = 0, from sum_eq_zero (λ i hi, by simp [wt i hi]), rw [hsum_t, add_zero] at h₁, rw [wp, add_zero, h₁, one_smul], - exact zi }, - { refine convex_iff_div.1 hs zi (ht hs₀ _ _) _ (sum_nonneg hs₀) h₁, - { exact lt_of_le_of_ne (sum_nonneg hs₀) (ne.symm hsum_t) }, - { intros j hj, exact hmem j (mem_insert_of_mem hj) }, - { exact h₀ _ (mem_insert_self _ _) } } + exact hpi }, + rw linear_combination_normalize hsum_t, + refine hs hpi _ (h₀ _ (mem_insert_self _ _)) (sum_nonneg ht₀) h₁, + refine ht (λ j hj, _) _ (λ j hj, hmem _ (mem_insert_of_mem hj)), + { dsimp, + refine mul_nonneg (inv_nonneg.2 (sum_nonneg ht₀)) (ht₀ j hj) }, + dsimp, + simp, --nonterminal simp to fix + rw [←mul_sum, inv_eq_one_div, one_div_mul_cancel hsum_t], end -lemma convex.sum_mem (hs : convex 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) +lemma _root_.convex.sum_mem (hs : convex 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hp : ∀ i ∈ t, p i ∈ s) : ∑ i in t, w i • p i ∈ s := -by simpa only [h₁, linear_combination, inv_one, one_smul] using - hs.linear_combination_mem h₀ (h₁.symm ▸ zero_lt_one) hz +hs.linear_combination_mem h₀ h₁ hp -lemma convex_iff_sum_mem : +lemma _root_.convex_iff_linear_combination_mem : convex 𝕜 s ↔ (∀ (t : finset E) (w : E → 𝕜), - (∀ i ∈ t, 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x in t, w x • x ∈ s ) := + (∀ 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, _⟩, + refine ⟨λ hs t w hw₀ hw₁ hts, hs.linear_combination_mem hw₀ hw₁ hts, _⟩, intros h x y hx hy a b ha hb hab, by_cases h_cases: x = y, { rw [h_cases, ←add_smul, hab, one_smul], exact hy }, - { convert h {x, y} (λ z, if p = y then b else a) _ _ _, + { convert h {x, y} (λ p, if p = y then b else a) _ _ _, { simp only [sum_pair h_cases, if_neg h_cases, if_pos rfl] }, { simp_intros i hi, cases hi; subst i; simp [ha, hb, if_neg h_cases] }, @@ -174,105 +188,111 @@ begin cases hi; subst i; simp [hx, hy, if_neg h_cases] } } end -lemma finset.linear_combination_mem_convex_hull (t : finset ι) {w : ι → 𝕜} (hw₀ : ∀ i ∈ t, 0 ≤ w i) - (hws : ∑ i in t, w i = 1) {p : ι → E} (hp : ∀ i ∈ t, p i ∈ s) : - s.linear_combination p w ∈ convex_hull 𝕜 s := -(convex_convex_hull 𝕜 s).linear_combination_mem hw₀ hws (λ i hi, subset_convex_hull 𝕜 s $ hp i hi) +lemma linear_combination_mem_convex_hull (t : finset ι) {w : ι → 𝕜} (hw₀ : ∀ i ∈ t, 0 ≤ w i) + (hwt : ∑ i in t, w i = 1) {p : ι → E} (hp : ∀ i ∈ t, p i ∈ s) : + t.linear_combination p w ∈ convex_hull 𝕜 s := +(convex_convex_hull 𝕜 s).linear_combination_mem hw₀ hwt (λ i hi, subset_convex_hull 𝕜 s $ hp 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`, `p '' 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 : ι → 𝕜) (p : ι → E) +/-- Convex hull of `s` is equal to the set of all linear combinations with sum `1` of `finset`s `t` +where `p '' t ⊆ s`. This version allows finsets in any type in any universe. -/ +lemma _root_.convex_hull_eq (s : set E) : + convex_hull 𝕜 s = {x : E | ∃ (ι : Type*) (t : finset ι) (w : ι → 𝕜) (p : ι → E) (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hp : ∀ i ∈ t, p i ∈ s), - s.linear_combination p w = x} := + t.linear_combination p w = x} := begin - refine subset.antisymm (convex_hull_min _ _) _, + refine (convex_hull_min _ _).antisymm _, { intros x hx, use [punit, {punit.star}, λ _, 1, λ _, x, λ _ _, zero_le_one, finset.sum_singleton, λ _ _, hx], simp only [finset.linear_combination, finset.sum_singleton, inv_one, one_smul] }, { rintros x y ⟨ι, sx, wx, zx, hwx₀, hwx₁, hzx, rfl⟩ ⟨ι', sy, wy, zy, hwy₀, hwy₁, hzy, rfl⟩ a b ha hb hab, - rw [finset.linear_combination_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab], + rw [finset.linear_combination_segment' _ _ _ _ _ _ _ _ hab], refine ⟨_, _, _, _, _, _, _, rfl⟩, { rintros i hi, rw [finset.mem_union, finset.mem_map, finset.mem_map] at hi, - rcases hi with ⟨j, hj, rfl⟩|⟨j, hj, rfl⟩; - simp only [sum.elim_inl, sum.elim_inr]; - apply_rules [mul_nonneg, hwx₀, hwy₀] }, + obtain ⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩ := hi, + { simp only [sum.elim_inl, function.embedding.inl_apply], + exact mul_nonneg ha (hwx₀ j hj) }, + { simp only [sum.elim_inr, function.embedding.inr_apply], + exact mul_nonneg hb (hwy₀ j hj) } }, { simp [finset.sum_sum_elim, finset.mul_sum.symm, *] }, { intros i hi, rw [finset.mem_union, finset.mem_map, finset.mem_map] at hi, rcases hi with ⟨j, hj, rfl⟩|⟨j, hj, rfl⟩; apply_rules [hzx, hzy] } }, - { rintros _ ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩, - exact s.linear_combination_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) hp } + { rintros _ ⟨ι, t, w, z, hw₀, hw₁, hp, rfl⟩, + exact t.linear_combination_mem_convex_hull hw₀ hw₁ hp } end -lemma finset.convex_hull_eq (s : finset E) : +protected lemma 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), - s.linear_combination w id = x} := + s.linear_combination id w = x} := begin - refine subset.antisymm (convex_hull_min _ _) _, + refine (convex_hull_min _ _).antisymm _, { intros x hx, rw [finset.mem_coe] at hx, - refine ⟨_, _, _, finset.linear_combination_ite_eq _ _ _ hx⟩, + refine ⟨_, _, _, finset.linear_combination_ite_eq _ _ id hx⟩, { intros, split_ifs, exacts [zero_le_one, le_refl 0] }, { rw [finset.sum_ite_eq, if_pos hx] } }, - { rintros x y ⟨wx, hwx₀, hwx₁, rfl⟩ ⟨wy, hwy₀, hwy₁, rfl⟩ - a b ha hb hab, - rw [finset.linear_combination_segment _ _ _ _ hwx₁ hwy₁ _ _ hab], + { rintro x y ⟨wx, hwx₀, hwx₁, rfl⟩ ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab, + rw [finset.linear_combination_segment _ _ _ _ _ _ hab], refine ⟨_, _, _, rfl⟩, { rintros i hi, apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀], }, { simp only [finset.sum_add_distrib, finset.mul_sum.symm, mul_one, *] } }, { rintros _ ⟨w, hw₀, hw₁, rfl⟩, exact s.linear_combination_mem_convex_hull (λ x hx, hw₀ _ hx) - (hw₁.symm ▸ zero_lt_one) (λ x hx, hx) } + hw₁ (λ x hx, hx) } end -lemma set.finite.convex_hull_eq {s : set E} (hs : finite s) : +lemma _root_.set.finite.convex_hull_eq {s : set E} (hs : finite s) : convex_hull 𝕜 s = {x : E | ∃ (w : E → 𝕜) (hw₀ : ∀ y ∈ s, 0 ≤ w y) - (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.linear_combination w id = x} := + (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.linear_combination id w = 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) : +lemma _root_.convex_hull_eq_union_convex_hull_finite_subsets (s : set E) : convex_hull 𝕜 s = ⋃ (t : finset E) (w : ↑t ⊆ s), convex_hull 𝕜 ↑t := begin - refine subset.antisymm _ _, + refine set.subset.antisymm _ _, { rw convex_hull_eq, - rintros x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩, + rintros x ⟨ι, t, w, p, hw₀, hw₁, hp, rfl⟩, simp only [mem_Union], - refine ⟨t.image z, _, _⟩, + refine ⟨t.image p, _, _⟩, { rw [coe_image, set.image_subset_iff], exact hp }, - { apply s.linear_combination_mem_convex_hull hw₀, + { apply t.linear_combination_mem_convex_hull hw₀, { simp only [hw₁, zero_lt_one] }, { exact λ i hi, finset.mem_coe.2 (finset.mem_image_of_mem _ hi) } } }, - { exact Union_subset (λ i, Union_subset convex_hull_mono), }, + { exact Union_subset (λ i, Union_subset convex_hull_mono) } end +end linear_ordered_field +end finset + /-! ### `std_simplex` -/ -variables (ι) [fintype ι] {f : ι → 𝕜} +section linear_ordered_field +variables (𝕜 E ι : Type*) [linear_ordered_field 𝕜] [add_comm_monoid E] [module 𝕜 E] [fintype ι] + (s : finset ι) /-- `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 𝕜 (range $ λ(i j:ι), if i = j then (1:𝕜) else (0 : 𝕜)) = std_simplex 𝕜 ι := begin - refine subset.antisymm (convex_hull_min _ (convex_std_simplex ι)) _, + refine (convex_hull_min _ (convex_std_simplex 𝕜 ι)).antisymm _, { rintros _ ⟨i, rfl⟩, - exact ite_eq_mem_std_simplex i }, + exact ite_eq_mem_std_simplex 𝕜 i }, { rintros w ⟨hw₀, hw₁⟩, - rw [pi_eq_sum_univ w, ← finset.univ.linear_combination_eq_of_sum_1 _ hw₁], + rw [pi_eq_sum_univ w], exact finset.univ.linear_combination_mem_convex_hull (λ i hi, hw₀ i) - (hw₁.symm ▸ zero_lt_one) (λ i hi, mem_range_self i) } + hw₁ (λ i hi, mem_range_self i) } end -variable {ι} +variables {𝕜 E ι} /-- The convex hull of a finite set is the image of the standard simplex in `s → 𝕜` under the linear map sending each function `w` to `∑ x in s, w x • x`. @@ -282,7 +302,7 @@ The map is defined in terms of operations on `(s → 𝕜) →ₗ[𝕜] 𝕜` so 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) := + (⇑(∑ x : s, (@linear_map.proj 𝕜 s _ (λ i, 𝕜) _ _ x).smul_right x.1)) '' (std_simplex 𝕜 s) := begin rw [← convex_hull_basis_eq_std_simplex, ← linear_map.convex_hull_image, ← set.range_comp, (∘)], apply congr_arg, @@ -292,6 +312,8 @@ 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) : +lemma mem_Icc_of_mem_std_simplex {f : ι → 𝕜} (hf : f ∈ std_simplex 𝕜 ι) (x) : f x ∈ Icc (0 : 𝕜) 1 := ⟨hf.1 x, hf.2 ▸ finset.single_le_sum (λ y hy, hf.1 y) (finset.mem_univ x)⟩ + +end linear_ordered_field diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index 004a86b2c4207..e2d5cd99226cf 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -13,14 +13,14 @@ inequality. The integral version can be found in `analysis.convex.integral`. A function `f : E → β` is `convex_on` a set `s` if `s` is itself a convex set, and for any two points `x y ∈ s`, the segment joining `(x, f x)` to `(y, f y)` is above the graph of `f`. -Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}` is +Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f z.1 ≤ p.2}` is a convex set. ## Main declarations * `convex_on 𝕜 s f`: The function `f` is convex on `s` with scalars `𝕜`. * `concave_on 𝕜 s f`: The function `f` is concave on `s` with scalars `𝕜`. -* `convex_on.map_center_mass_le` `convex_on.map_sum_le`: Convex Jensen's inequality. +* `convex_on.map_linear_combination_le` `convex_on.map_sum_le`: Convex Jensen's inequality. -/ open finset linear_map set @@ -131,7 +131,7 @@ lemma linear_order.concave_on_of_lt {f : E → β} [linear_order E] (hs : convex /-- For a function `f` defined on a convex subset `D` of `ℝ`, if for any three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope -of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity +of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of zroving convexity of a function is used in the proof of convexity of a function with a monotone derivative. -/ lemma convex_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex ℝ s) {f : ℝ → ℝ} (hf : ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z → @@ -534,57 +534,57 @@ by simpa only [add_comm] using hf.translate_right /-! ### Jensen's inequality -/ -variables {i j : ι} {c : ℝ} {t : finset ι} {w : ι → ℝ} {z : ι → E} +variables {i j : ι} {c : ℝ} {t : finset ι} {w : ι → ℝ} {p : ι → E} -/-- Convex **Jensen's inequality**, `finset.center_mass` version. -/ -lemma convex_on.map_center_mass_le {f : E → ℝ} (hf : convex_on s f) - (h₀ : ∀ i ∈ t, 0 ≤ w i) (hpos : 0 < ∑ i in t, w i) - (hmem : ∀ i ∈ t, z i ∈ s) : f (t.center_mass w z) ≤ t.center_mass w (f ∘ z) := +/-- Convex **Jensen's inequality**, `finset.linear_combination` version. -/ +lemma convex_on.map_linear_combination_le {f : E → ℝ} (hf : convex_on s f) + (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) + (hmem : ∀ i ∈ t, p i ∈ s) : f (t.linear_combination p w) ≤ t.linear_combination (f ∘ p) w := begin - have hmem' : ∀ i ∈ t, (z i, (f ∘ z) i) ∈ {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}, + have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}, from λ i hi, ⟨hmem i hi, le_rfl⟩, - convert (hf.convex_epigraph.center_mass_mem h₀ hpos hmem').2; - simp only [center_mass, function.comp, prod.smul_fst, prod.fst_sum, prod.smul_snd, prod.snd_sum] + convert (hf.convex_epigraph.linear_combination_mem h₀ h₁ hmem').2; + simp only [linear_combination, function.comp, prod.smul_fst, prod.fst_sum, + prod.smul_snd, prod.snd_sum] end /-- Convex **Jensen's inequality**, `finset.sum` version. -/ lemma convex_on.map_sum_le {f : E → ℝ} (hf : convex_on s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) - (hmem : ∀ i ∈ t, z i ∈ s) : f (∑ i in t, w i • z i) ≤ ∑ i in t, w i * (f (z i)) := -by simpa only [center_mass, h₁, inv_one, one_smul] - using hf.map_center_mass_le h₀ (h₁.symm ▸ zero_lt_one) hmem + (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i in t, w i • p i) ≤ ∑ i in t, w i * (f (p i)) := +by simpa only [linear_combination, h₁, inv_one, one_smul] + using hf.map_linear_combination_le h₀ h₁ hmem -/-! ### Maximal principle -/ +/-! ### Maximum principle -/ /-- If a function `f` is convex on `s` takes value `y` at the center of mass of some points -`z i ∈ s`, then for some `i` we have `y ≤ f (z i)`. -/ -lemma convex_on.exists_ge_of_center_mass {f : E → ℝ} (h : convex_on s f) - (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hws : 0 < ∑ i in t, w i) (hz : ∀ i ∈ t, z i ∈ s) : - ∃ i ∈ t, f (t.center_mass w z) ≤ f (z i) := +`p i ∈ s`, then for some `i` we have `y ≤ f (p i)`. -/ +lemma convex_on.exists_ge_of_linear_combination {f : E → ℝ} (h : convex_on s f) + (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, p i ∈ s) : + ∃ i ∈ t, f (t.linear_combination p w) ≤ f (p i) := begin - set y := t.center_mass w z, - have : f y ≤ t.center_mass w (f ∘ z) := h.map_center_mass_le hw₀ hws hz, - rw ← sum_filter_ne_zero at hws, - rw [← finset.center_mass_filter_ne_zero (f ∘ z), center_mass, smul_eq_mul, - ← div_eq_inv_mul, le_div_iff hws, mul_sum] at this, - replace : ∃ i ∈ t.filter (λ i, w i ≠ 0), f y * w i ≤ w i • (f ∘ z) i := - exists_le_of_sum_le (nonempty_of_sum_ne_zero (ne_of_gt hws)) this, - rcases this with ⟨i, hi, H⟩, - rw [mem_filter] at hi, - use [i, hi.1], - simp only [smul_eq_mul, mul_comm (w i)] at H, - refine (mul_le_mul_right _).1 H, - exact lt_of_le_of_ne (hw₀ i hi.1) hi.2.symm + set y := t.linear_combination p w, + suffices h : ∃ i ∈ t.filter (λ i, w i ≠ 0), w i • f y ≤ w i • (f ∘ p) i, + { obtain ⟨i, hi, hfi⟩ := h, + rw mem_filter at hi, + exact ⟨i, hi.1, (smul_le_smul_iff_of_pos $ (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩ }, + refine exists_le_of_sum_le _ _, + { have := @zero_ne_one ℝ _ _, + rw [←hw₁, ←sum_filter_ne_zero] at this, + exact nonempty_of_sum_ne_zero this.symm }, + { rw [←linear_combination, ←linear_combination, finset.linear_combination_filter_ne_zero, + finset.linear_combination_filter_ne_zero, linear_combination_const_left, hw₁, one_smul], + exact h.map_linear_combination_le hw₀ hw₁ hz } end /-- Maximum principle for convex functions. If a function `f` is convex on the convex hull of `s`, -then `f` can't have a maximum on `convex_hull s` outside of `s`. -/ +then `f` reaches a maximum on `convex_hull ℝ s` outside of `s`. -/ lemma convex_on.exists_ge_of_mem_convex_hull {f : E → ℝ} (hf : convex_on (convex_hull ℝ s) f) {x} (hx : x ∈ convex_hull ℝ s) : ∃ y ∈ s, f x ≤ f y := begin - rw _root_.convex_hull_eq at hx, - rcases hx with ⟨α, t, w, z, hw₀, hw₁, hz, rfl⟩, - rcases hf.exists_ge_of_center_mass hw₀ (hw₁.symm ▸ zero_lt_one) - (λ i hi, subset_convex_hull ℝ s (hz i hi)) with ⟨i, hit, Hi⟩, - exact ⟨z i, hz i hit, Hi⟩ + rw convex_hull_eq at hx, + obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx, + rcases hf.exists_ge_of_linear_combination hw₀ hw₁ + (λ i hi, subset_convex_hull ℝ s (hp i hi)) with ⟨i, hit, Hi⟩, + exact ⟨p i, hp i hit, Hi⟩ end diff --git a/src/analysis/convex/independent.lean b/src/analysis/convex/independent.lean index 5820633ea6177..75fb00a7ca937 100644 --- a/src/analysis/convex/independent.lean +++ b/src/analysis/convex/independent.lean @@ -33,7 +33,7 @@ convex independence. ## TODO Prove `affine_independent.convex_independent`. This requires some glue between `affine_combination` -and `finset.center_mass`. +and `finset.linear_combination`. ## Tags diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index d7cb6f9bd4611..fd27f37592b1c 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -13,8 +13,8 @@ In this file we prove four theorems: * `convex.smul_integral_mem`: if `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the average value - of `f` belongs to `s`: `(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` - for a finite sum version of this lemma. + of `f` belongs to `s`: `(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also + `convex.linear_combination_mem` for a finite sum version of this lemma. * `convex.integral_mem`: if `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` @@ -25,7 +25,7 @@ In this file we prove four theorems: continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to the average value of `g ∘ f` provided that both `f` and `g ∘ f` are - integrable. See also `convex.map_center_mass_le` for a finite sum version of this lemma. + integrable. See also `convex.map_linear_combination_le` for a finite sum version of this lemma. * `convex_on.map_integral_le`: Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a @@ -66,7 +66,7 @@ begin by rw [← (F n).sum_range_measure_preimage_singleton, @ennreal.to_real_sum _ _ (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_lt_top _ _))], rw [← this, simple_func.integral], - refine hs.center_mass_mem (λ _ _, ennreal.to_real_nonneg) _ _, + refine hs.linear_combination_mem (λ _ _, ennreal.to_real_nonneg) _ _, { rw [this, ennreal.to_real_pos_iff, pos_iff_ne_zero, ne.def, measure.measure_univ_eq_zero], exact ⟨hμ, measure_ne_top _ _⟩ }, { simp only [simple_func.mem_range], @@ -76,8 +76,8 @@ end /-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`: -`(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` for a finite sum version -of this lemma. -/ +`(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.linear_combination_mem` for a finite sum +version of this lemma. -/ lemma convex.smul_integral_mem [is_finite_measure μ] {s : set E} (hs : convex ℝ s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) : @@ -104,8 +104,8 @@ by simpa [measure_univ] using hs.smul_integral_mem hsc (is_probability_measure.n /-- Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to the average value -of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_center_mass_le` -for a finite sum version of this lemma. -/ +of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also +`convex.map_linear_combination_le` for a finite sum version of this lemma. -/ lemma convex_on.map_smul_integral_le [is_finite_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) : diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean index 8b5effcbf0858..46caa3544bcda 100644 --- a/src/analysis/convex/topology.lean +++ b/src/analysis/convex/topology.lean @@ -41,9 +41,9 @@ section std_simplex variables [fintype ι] -/-- Every vector in `std_simplex ι` has `max`-norm at most `1`. -/ +/-- 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], @@ -55,18 +55,18 @@ end variable (ι) -/-- `std_simplex ι` is bounded. -/ -lemma bounded_std_simplex : metric.bounded (std_simplex ι) := +/-- `std_simplex ℝ ι` is bounded. -/ +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 +/-- `std_simplex ℝ ι` is closed. -/ +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 ι) := +/-- `std_simplex ℝ ι` is compact. -/ +lemma compact_std_simplex : is_compact (std_simplex ℝ ι) := metric.compact_iff_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩ end std_simplex From 665aeafec8841364947e04e7029bdf7345f37133 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Tue, 21 Sep 2021 16:31:22 +0200 Subject: [PATCH 04/17] break long line --- src/analysis/convex/combination.lean | 8 ++++++-- src/analysis/convex/function.lean | 2 +- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index b4f9a28adca49..9f4ec42d85748 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -9,8 +9,12 @@ import analysis.convex.basic # Linear combinations This file defines linear combinations of points in a semimodule and proves results about convex -combinations. Convex combinations in a semimodule can be modelled as linear combinations with -nonnegative coefficients summing to `1`. In an affine space, they can be modelled through affine combinations. +combinations. + +Convex combinations in a semimodule can be modelled as linear combinations with nonnegative coefficients summing to `1`. In an affine space, they can be modelled through affine combinations. + +In a vector space, both coincide but it is still an open question whether we can make the two ways +to derive `convex_combination` definitionally equal. ## Main declarations diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index e2d5cd99226cf..fb9cab39f5528 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -131,7 +131,7 @@ lemma linear_order.concave_on_of_lt {f : E → β} [linear_order E] (hs : convex /-- For a function `f` defined on a convex subset `D` of `ℝ`, if for any three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope -of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of zroving convexity +of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity of a function is used in the proof of convexity of a function with a monotone derivative. -/ lemma convex_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex ℝ s) {f : ℝ → ℝ} (hf : ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z → From e16df20f7a44f9c8fc8b54f57aa8b6c48e4e9b1e Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Tue, 21 Sep 2021 16:45:36 +0200 Subject: [PATCH 05/17] make convex.sum_mem useful --- src/analysis/convex/combination.lean | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 9f4ec42d85748..3781e5c506241 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -163,16 +163,26 @@ begin refine hs hpi _ (h₀ _ (mem_insert_self _ _)) (sum_nonneg ht₀) h₁, refine ht (λ j hj, _) _ (λ j hj, hmem _ (mem_insert_of_mem hj)), { dsimp, - refine mul_nonneg (inv_nonneg.2 (sum_nonneg ht₀)) (ht₀ j hj) }, + exact mul_nonneg (inv_nonneg.2 (sum_nonneg ht₀)) (ht₀ j hj) }, dsimp, simp, --nonterminal simp to fix rw [←mul_sum, inv_eq_one_div, one_div_mul_cancel hsum_t], end -lemma _root_.convex.sum_mem (hs : convex 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) +lemma _root_.convex.sum_mem (hs : convex 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i ≠ 0) (hp : ∀ i ∈ t, p i ∈ s) : - ∑ i in t, w i • p i ∈ s := -hs.linear_combination_mem h₀ h₁ hp + (∑ i in t, w i)⁻¹ • ∑ i in t, w i • p i ∈ s := +begin + rw [linear_combination_normalize h₁, inv_smul_smul' h₁], + refine hs.linear_combination_mem _ _ hp, + { + rintro i hi, + refine smul_nonneg (h₀ i hi) _, + sorry + }, + { rw [smul_sum, div_self h₁], + } +end lemma _root_.convex_iff_linear_combination_mem : convex 𝕜 s ↔ From 4b2bba427a1809a36da5ee2006303909325f8f5f Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Tue, 21 Sep 2021 20:14:43 +0200 Subject: [PATCH 06/17] restore convex.linear_combination_mem --- src/analysis/convex/combination.lean | 21 +++++++-------------- src/analysis/convex/integral.lean | 6 +++--- 2 files changed, 10 insertions(+), 17 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 3781e5c506241..1fe29bbec967a 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -164,24 +164,17 @@ begin refine ht (λ j hj, _) _ (λ j hj, hmem _ (mem_insert_of_mem hj)), { dsimp, exact mul_nonneg (inv_nonneg.2 (sum_nonneg ht₀)) (ht₀ j hj) }, - dsimp, - simp, --nonterminal simp to fix - rw [←mul_sum, inv_eq_one_div, one_div_mul_cancel hsum_t], + { simp_rw [pi.smul_apply, ←smul_sum, smul_eq_mul, inv_mul_cancel hsum_t] } end -lemma _root_.convex.sum_mem (hs : convex 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i ≠ 0) - (hp : ∀ i ∈ t, p i ∈ s) : - (∑ i in t, w i)⁻¹ • ∑ i in t, w i • p i ∈ s := +lemma _root_.convex.linear_combination_mem' (hs : convex 𝕜 s) (h₀ : ∀ i ∈ t, 0 ≤ w i) + (h₁ : ∑ i in t, w i ≠ 0) (hp : ∀ i ∈ t, p i ∈ s) : + (∑ i in t, w i)⁻¹ • t.linear_combination p w ∈ s := begin rw [linear_combination_normalize h₁, inv_smul_smul' h₁], - refine hs.linear_combination_mem _ _ hp, - { - rintro i hi, - refine smul_nonneg (h₀ i hi) _, - sorry - }, - { rw [smul_sum, div_self h₁], - } + refine hs.linear_combination_mem (λ i hi, mul_nonneg (inv_nonneg.2 $ sum_nonneg h₀) + (h₀ i hi)) _ hp, + simp_rw [pi.smul_apply, ←smul_sum, smul_eq_mul, inv_mul_cancel h₁] end lemma _root_.convex_iff_linear_combination_mem : diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index b35a025ac942e..66ec3aa9c0615 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -18,8 +18,8 @@ In this file we prove four theorems: * `convex.integral_mem`: if `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` - belongs to `s`: `∫ x, f x ∂μ ∈ s`. See also `convex.sum_mem` for a finite sum version of this - lemma. + belongs to `s`: `∫ x, f x ∂μ ∈ s`. See also `convex.linear_combination_mem` for a finite sum + version of this lemma. * `convex_on.map_smul_integral_le`: Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is @@ -66,7 +66,7 @@ begin by rw [← (F n).sum_range_measure_preimage_singleton, @ennreal.to_real_sum _ _ (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_ne_top _ _))], rw [← this, simple_func.integral], - refine hs.linear_combination_mem (λ _ _, ennreal.to_real_nonneg) _ _, + refine hs.linear_combination_mem' (λ _ _, ennreal.to_real_nonneg) _ _, { rw [this, ennreal.to_real_pos_iff, pos_iff_ne_zero, ne.def, measure.measure_univ_eq_zero], exact ⟨hμ, measure_ne_top _ _⟩ }, { simp only [simple_func.mem_range], From 56743d978391ab8bd604cf4951eabacb5e5c5e81 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Wed, 22 Sep 2021 09:34:14 +0200 Subject: [PATCH 07/17] fix analysis.convex.integral --- src/analysis/convex/combination.lean | 3 ++- src/analysis/convex/integral.lean | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 1fe29bbec967a..708d3f31c1461 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -11,7 +11,8 @@ import analysis.convex.basic This file defines linear combinations of points in a semimodule and proves results about convex combinations. -Convex combinations in a semimodule can be modelled as linear combinations with nonnegative coefficients summing to `1`. In an affine space, they can be modelled through affine combinations. +Convex combinations in a semimodule can be modelled as linear combinations with nonnegative +coefficients summing to `1`. In an affine space, they can be modelled through affine combinations. In a vector space, both coincide but it is still an open question whether we can make the two ways to derive `convex_combination` definitionally equal. diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index 66ec3aa9c0615..793bbe5e9e42f 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -67,8 +67,8 @@ begin (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_ne_top _ _))], rw [← this, simple_func.integral], refine hs.linear_combination_mem' (λ _ _, ennreal.to_real_nonneg) _ _, - { rw [this, ennreal.to_real_pos_iff, pos_iff_ne_zero, ne.def, measure.measure_univ_eq_zero], - exact ⟨hμ, measure_ne_top _ _⟩ }, + { rw [this, ne.def, ennreal.to_real_eq_zero_iff, measure.measure_univ_eq_zero], + exact not_or hμ (measure_ne_top _ _) }, { simp only [simple_func.mem_range], rintros _ ⟨x, rfl⟩, exact simple_func.approx_on_mem hfm h₀ n x } From 5d3c959cc46da48a983ad6bfd3fac4879ca56e0e Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Wed, 22 Sep 2021 14:11:28 +0200 Subject: [PATCH 08/17] remove unused arguments --- src/analysis/convex/combination.lean | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 708d3f31c1461..c62ef2c991974 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -44,9 +44,6 @@ section ordered_semiring variables {𝕜 E ι ι' : Type*} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (i j : ι) (c : 𝕜) (s : finset ι) (p : ι → E) (w : ι → 𝕜) -lemma linear_combination_def : - s.linear_combination p w = ∑ i in s, w i • p i := rfl - lemma linear_combination_empty : (∅ : finset ι).linear_combination p w = 0 := by simp only [linear_combination, sum_empty, smul_zero] @@ -71,7 +68,7 @@ by rw [linear_combination, finset.sum_smul] /-- A convex combination of two centers of mass is a center of mass as well. This version deals with two different index types. -/ lemma linear_combination_segment' (s : finset ι) (t : finset ι') (ws : ι → 𝕜) (ps : ι → E) - (wt : ι' → 𝕜) (pt : ι' → E) (a b : 𝕜) (hab : a + b = 1) : + (wt : ι' → 𝕜) (pt : ι' → E) (a b : 𝕜) : a • s.linear_combination ps ws + b • t.linear_combination pt wt = (s.map function.embedding.inl ∪ t.map function.embedding.inr).linear_combination (sum.elim ps pt) @@ -84,13 +81,12 @@ 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 linear_combination_segment (s : finset ι) (w₁ w₂ : ι → 𝕜) (p : ι → E) (a b : 𝕜) - (hab : a + b = 1) : +lemma linear_combination_segment (s : finset ι) (w₁ w₂ : ι → 𝕜) (p : ι → E) (a b : 𝕜) : a • s.linear_combination p w₁ + b • s.linear_combination p w₂ = s.linear_combination p (λ i, a * w₁ i + b * w₂ i) := begin unfold linear_combination, - simp only [linear_combination_def, smul_sum, sum_add_distrib, add_smul, mul_smul, *], + simp only [linear_combination, smul_sum, sum_add_distrib, add_smul, mul_smul, *], end lemma linear_combination_ite_eq (hi : i ∈ s) : @@ -217,7 +213,7 @@ begin simp only [finset.linear_combination, finset.sum_singleton, inv_one, one_smul] }, { rintros x y ⟨ι, sx, wx, zx, hwx₀, hwx₁, hzx, rfl⟩ ⟨ι', sy, wy, zy, hwy₀, hwy₁, hzy, rfl⟩ a b ha hb hab, - rw [finset.linear_combination_segment' _ _ _ _ _ _ _ _ hab], + rw [finset.linear_combination_segment' _ _ _ _ _ _ _ _], refine ⟨_, _, _, _, _, _, _, rfl⟩, { rintros i hi, rw [finset.mem_union, finset.mem_map, finset.mem_map] at hi, @@ -245,7 +241,7 @@ begin { intros, split_ifs, exacts [zero_le_one, le_refl 0] }, { rw [finset.sum_ite_eq, if_pos hx] } }, { rintro x y ⟨wx, hwx₀, hwx₁, rfl⟩ ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab, - rw [finset.linear_combination_segment _ _ _ _ _ _ hab], + rw [finset.linear_combination_segment _ _ _ _ _ _], refine ⟨_, _, _, rfl⟩, { rintros i hi, apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀], }, From 3a4e7b5e68c26dbcffcbea76e1cfed0376a8d6d3 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Wed, 22 Sep 2021 17:55:53 +0200 Subject: [PATCH 09/17] initial commit --- src/analysis/convex/basic.lean | 8 +- src/analysis/convex/function.lean | 371 ++++++++++++++++-------------- 2 files changed, 208 insertions(+), 171 deletions(-) diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean index 6eca9c847b8e0..7754a4fedd2e0 100644 --- a/src/analysis/convex/basic.lean +++ b/src/analysis/convex/basic.lean @@ -119,7 +119,7 @@ begin exact h (mem_open_segment_of_ne_left_right 𝕜 hxz hyz hz), end -lemma convex.combo_self {x y : 𝕜} (h : x + y = 1) (a : 𝕜) : x • a + y • a = a := +lemma convex.combo_self {x y : 𝕜} (h : x + y = 1) (a : E) : x • a + y • a = a := by rw [←add_smul, h, one_smul] end ordered_semiring @@ -401,14 +401,14 @@ section ordered_semiring variables [ordered_semiring 𝕜] section add_comm_monoid -variables [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] +variables [add_comm_monoid E] /-- Convexity of sets. -/ -def convex (s : set E) := +def convex [has_scalar 𝕜 E](s : set E) := ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s -variables {𝕜} {s : set E} +variables {𝕜} [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] {s : set E} lemma convex_iff_forall_pos : convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index fb9cab39f5528..e34b897015d0e 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -13,74 +13,141 @@ inequality. The integral version can be found in `analysis.convex.integral`. A function `f : E → β` is `convex_on` a set `s` if `s` is itself a convex set, and for any two points `x y ∈ s`, the segment joining `(x, f x)` to `(y, f y)` is above the graph of `f`. -Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f z.1 ≤ p.2}` is +Equivalently, `convex_on 𝕜 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f z.1 ≤ p.2}` is a convex set. ## Main declarations -* `convex_on 𝕜 s f`: The function `f` is convex on `s` with scalars `𝕜`. -* `concave_on 𝕜 s f`: The function `f` is concave on `s` with scalars `𝕜`. +* `convex_on 𝕜 𝕜 s f`: The function `f` is convex on `s` with scalars `𝕜`. +* `concave_on 𝕜 𝕜 s f`: The function `f` is concave on `s` with scalars `𝕜`. * `convex_on.map_linear_combination_le` `convex_on.map_sum_le`: Convex Jensen's inequality. -/ open finset linear_map set open_locale big_operators classical convex pointwise -variables {𝕜 E F ι ι' β : Type*} [add_comm_group E] [module ℝ E] [add_comm_group F] [module ℝ F] - [ordered_add_comm_monoid β] [module ℝ β] {s : set E} +variables (𝕜 : Type*) {E F ι ι' β : Type*} + +section ordered_semiring +variables [ordered_semiring 𝕜] [add_comm_monoid E] + +section ordered_add_comm_monoid +variables [ordered_add_comm_monoid β] /-- Convexity of functions -/ -def convex_on (s : set E) (f : E → β) : Prop := - convex ℝ s ∧ - ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → +def convex_on [has_scalar 𝕜 E] [has_scalar 𝕜 β] (s : set E) (f : E → β) : Prop := +convex 𝕜 s ∧ + ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y /-- Concavity of functions -/ -def concave_on (s : set E) (f : E → β) : Prop := - convex ℝ s ∧ - ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → +def concave_on [has_scalar 𝕜 E] [has_scalar 𝕜 β] (s : set E) (f : E → β) : Prop := +convex 𝕜 s ∧ + ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y) +section has_scalar +variables {𝕜} [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} + +lemma convex_on_id {s : set 𝕜} (hs : convex 𝕜 s) : convex_on 𝕜 s id := ⟨hs, by { intros, refl }⟩ + +lemma concave_on_id {s : set 𝕜} (hs : convex 𝕜 s) : concave_on 𝕜 s id := ⟨hs, by { intros, refl }⟩ + +end has_scalar + +section module +variables {𝕜} [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} +lemma convex_on_const (c : β) (hs : convex 𝕜 s) : convex_on 𝕜 s (λ x:E, c) := +⟨hs, λ x y _ _ a b _ _ hab, (convex.combo_self hab c).ge⟩ + +lemma concave_on_const (c : β) (hs : convex 𝕜 s) : concave_on 𝕜 s (λ x:E, c) := +@convex_on_const _ _ (order_dual β) _ _ _ _ _ _ c hs + +end module + +section module +variables {𝕜} [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} + +/-- For a function on a convex set in a linear ordered space, in order to prove that it is convex +it suffices to verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` +and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with +lexicographic order. -/ +lemma linear_order.convex_on_of_lt (hs : convex 𝕜 s) + (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → + f (a • x + b • y) ≤ a • f x + b • f y) : convex_on 𝕜 s f := +begin + use hs, + intros x y hx hy a b ha hb hab, + wlog hxy : x ≤ y using [x y a b, y x b a], + { exact le_total _ _ }, + obtain rfl | hxy := hxy.eq_or_lt, + { rw [convex.combo_self hab, convex.combo_self hab] }, + obtain rfl | ha' := ha.eq_or_lt, + { rw [zero_add] at hab, subst b, simp_rw [zero_smul, zero_add, one_smul] }, + obtain rfl | hb' := hb.eq_or_lt, + { rw [add_zero] at hab, subst a }, + exact hf hx hy hxy ha' hb' hab, +end + +/-- For a function on a convex set in a linear ordered space, in order to prove that it is concave +it suffices to verify the inequality `a • f x + b • f y ≤ f (a • x + b • y)` only for `x < y` +and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with +lexicographic order. -/ +lemma linear_order.concave_on_of_lt (hs : convex 𝕜 s) + (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → + a • f x + b • f y ≤ f (a • x + b • y)) : concave_on 𝕜 s f := +@linear_order.convex_on_of_lt _ _ (order_dual β) _ _ _ _ _ f _ hs hf + +end module + +end ordered_add_comm_monoid + +section ordered_add_comm_group +variables [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] + section -variables [ordered_smul ℝ β] +variables {𝕜} -/-- A function `f` is concave iff `-f` is convex. -/ -@[simp] lemma neg_convex_on_iff {γ : Type*} [ordered_add_comm_group γ] [module ℝ γ] - (s : set E) (f : E → γ) : convex_on s (-f) ↔ concave_on s f := +/-- A function `-f` is convex iff `f` is concave. -/ +@[simp] lemma neg_concave_on_iff + (s : set E) (f : E → β) : convex_on 𝕜 s (-f) ↔ concave_on 𝕜 s f := begin split, - { rintros ⟨hconv, h⟩, + { rintro ⟨hconv, h⟩, refine ⟨hconv, _⟩, intros x y xs ys a b ha hb hab, specialize h xs ys ha hb hab, simp [neg_apply, neg_le, add_comm] at h, exact h }, - { rintros ⟨hconv, h⟩, + { rintro ⟨hconv, h⟩, refine ⟨hconv, _⟩, intros x y xs ys a b ha hb hab, specialize h xs ys ha hb hab, simp [neg_apply, neg_le, add_comm, h] } end -/-- A function `f` is concave iff `-f` is convex. -/ -@[simp] lemma neg_concave_on_iff {γ : Type*} [ordered_add_comm_group γ] [module ℝ γ] - (s : set E) (f : E → γ) : concave_on s (-f) ↔ convex_on s f:= -by rw [← neg_convex_on_iff s (-f), neg_neg f] +/-- A function `-f` is concave iff `f` is convex. -/ +@[simp] lemma neg_convex_on_iff {γ : Type*} [ordered_add_comm_group γ] [module 𝕜 γ] + (s : set E) (f : E → γ) : concave_on 𝕜 s (-f) ↔ convex_on 𝕜 s f:= +by rw [← neg_concave_on_iff s (-f), neg_neg f] end -lemma convex_on_id {s : set ℝ} (hs : convex ℝ s) : convex_on s id := ⟨hs, by { intros, refl }⟩ +end ordered_add_comm_group + +end ordered_semiring -lemma concave_on_id {s : set ℝ} (hs : convex ℝ s) : concave_on s id := ⟨hs, by { intros, refl }⟩ +section linear_ordered_field +variables {𝕜} [linear_ordered_field 𝕜] [add_comm_monoid E] -lemma convex_on_const (c : β) (hs : convex ℝ s) : convex_on s (λ x:E, c) := -⟨hs, by { intros, simp only [← add_smul, *, one_smul] }⟩ +section ordered_add_comm_monoid +variables [ordered_add_comm_monoid β] -lemma concave_on_const (c : β) (hs : convex ℝ s) : concave_on s (λ x:E, c) := -@convex_on_const _ (order_dual β) _ _ _ _ _ c hs +section has_scalar +variables [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} lemma convex_on_iff_div {f : E → β} : - convex_on s f ↔ convex ℝ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b + convex_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → f ((a/(a+b)) • x + (b/(a+b)) • y) ≤ (a/(a+b)) • f x + (b/(a+b)) • f y := and_congr iff.rfl ⟨begin @@ -95,48 +162,18 @@ begin end⟩ lemma concave_on_iff_div {f : E → β} : - concave_on s f ↔ convex ℝ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → 0 < a + b + concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a/(a+b)) • f x + (b/(a+b)) • f y ≤ f ((a/(a+b)) • x + (b/(a+b)) • y) := -@convex_on_iff_div _ (order_dual β) _ _ _ _ _ _ - -/-- For a function on a convex set in a linear ordered space, in order to prove that it is convex -it suffices to verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` -and positive `a`, `b`. The main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with -lexicographic order. -/ -lemma linear_order.convex_on_of_lt {f : E → β} [linear_order E] (hs : convex ℝ s) - (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → - f (a • x + b • y) ≤ a • f x + b • f y) : convex_on s f := -begin - use hs, - intros x y hx hy a b ha hb hab, - wlog hxy : x<=y using [x y a b, y x b a], - { exact le_total _ _ }, - { cases eq_or_lt_of_le hxy with hxy hxy, - by { subst y, rw [← add_smul, ← add_smul, hab, one_smul, one_smul] }, - cases eq_or_lt_of_le ha with ha ha, - by { subst a, rw [zero_add] at hab, subst b, simp }, - cases eq_or_lt_of_le hb with hb hb, - by { subst b, rw [add_zero] at hab, subst a, simp }, - exact hf hx hy hxy ha hb hab } -end - -/-- For a function on a convex set in a linear ordered space, in order to prove that it is concave -it suffices to verify the inequality `a • f x + b • f y ≤ f (a • x + b • y)` only for `x < y` -and positive `a`, `b`. The main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with -lexicographic order. -/ -lemma linear_order.concave_on_of_lt {f : E → β} [linear_order E] (hs : convex ℝ s) - (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → - a • f x + b • f y ≤ f (a • x + b • y)) : concave_on s f := -@linear_order.convex_on_of_lt _ (order_dual β) _ _ _ _ _ f _ hs hf +@convex_on_iff_div _ _ (order_dual β) _ _ _ _ _ _ _ -/-- For a function `f` defined on a convex subset `D` of `ℝ`, if for any three points `x < y < z` +/-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity of a function is used in the proof of convexity of a function with a monotone derivative. -/ -lemma convex_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex ℝ s) {f : ℝ → ℝ} - (hf : ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z → +lemma convex_on_real_of_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} + (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) : - convex_on s f := + convex_on 𝕜 s f := linear_order.convex_on_of_lt hs begin assume x z hx hz hxz a b ha hb hab, @@ -158,11 +195,11 @@ begin convert this; symmetry; simp only [div_eq_iff (ne_of_gt B), y]; ring end -/-- For a function `f` defined on a subset `D` of `ℝ`, if `f` is convex on `D`, then for any three +/-- For a function `f` defined on a subset `D` of `𝕜`, if `f` is convex on `D`, then for any three points `x < y < z`, the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope of the secant line of `f` on `[x, z]`. -/ -lemma convex_on.slope_mono_adjacent {s : set ℝ} {f : ℝ → ℝ} (hf : convex_on s f) - {x y z : ℝ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : +lemma convex_on.slope_mono_adjacent {s : set 𝕜} {f : 𝕜 → 𝕜} (hf : convex_on 𝕜 s f) + {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) := begin have h₁ : 0 < y - x := by linarith, @@ -186,21 +223,21 @@ begin { nlinarith, }, end -/-- For a function `f` defined on a convex subset `D` of `ℝ`, `f` is convex on `D` iff, for any +/-- For a function `f` defined on a convex subset `D` of `𝕜`, `f` is convex on `D` iff, for any three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope,of the secant line of `f` on `[x, z]`. -/ -lemma convex_on_real_iff_slope_mono_adjacent {s : set ℝ} (hs : convex ℝ s) {f : ℝ → ℝ} : - convex_on s f ↔ - (∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z → +lemma convex_on_real_iff_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} : + convex_on 𝕜 s f ↔ + (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) := ⟨convex_on.slope_mono_adjacent, convex_on_real_of_slope_mono_adjacent hs⟩ -/-- For a function `f` defined on a convex subset `D` of `ℝ`, if for any three points `x < y < z` +/-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is greater than or equal to the slope of the secant line of `f` on `[x, z]`, then `f` is concave on `D`. -/ -lemma concave_on_real_of_slope_mono_adjacent {s : set ℝ} (hs : convex ℝ s) {f : ℝ → ℝ} - (hf : ∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z → - (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) : concave_on s f := +lemma concave_on_real_of_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} + (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → + (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) : concave_on 𝕜 s f := begin rw [←neg_convex_on_iff], apply convex_on_real_of_slope_mono_adjacent hs, @@ -209,11 +246,11 @@ begin simp only [hf xs zs xy yz, neg_sub_neg, pi.neg_apply], end -/-- For a function `f` defined on a subset `D` of `ℝ`, if `f` is concave on `D`, then for any three +/-- For a function `f` defined on a subset `D` of `𝕜`, if `f` is concave on `D`, then for any three points `x < y < z`, the slope of the secant line of `f` on `[x, y]` is greater than or equal to the slope of the secant line of `f` on `[x, z]`. -/ -lemma concave_on.slope_mono_adjacent {s : set ℝ} {f : ℝ → ℝ} (hf : concave_on s f) - {x y z : ℝ} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : +lemma concave_on.slope_mono_adjacent {s : set 𝕜} {f : 𝕜 → 𝕜} (hf : concave_on 𝕜 s f) + {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f z - f y) / (z - y) ≤ (f y - f x) / (y - x) := begin rw [←neg_le_neg_iff, ←neg_div, ←neg_div, neg_sub, neg_sub], @@ -223,29 +260,29 @@ begin apply convex_on.slope_mono_adjacent hf; assumption, end -/-- For a function `f` defined on a convex subset `D` of `ℝ`, `f` is concave on `D` iff for any +/-- For a function `f` defined on a convex subset `D` of `𝕜`, `f` is concave on `D` iff for any three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is greater than or equal to the slope of the secant line of `f` on `[x, z]`. -/ -lemma concave_on_real_iff_slope_mono_adjacent {s : set ℝ} (hs : convex ℝ s) {f : ℝ → ℝ} : - concave_on s f ↔ - (∀ {x y z : ℝ}, x ∈ s → z ∈ s → x < y → y < z → +lemma concave_on_real_iff_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} : + concave_on 𝕜 s f ↔ + (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) := ⟨concave_on.slope_mono_adjacent, concave_on_real_of_slope_mono_adjacent hs⟩ -lemma convex_on.subset {f : E → β} {t : set E} (h_convex_on : convex_on t f) - (h_subset : s ⊆ t) (h_convex : convex ℝ s) : convex_on s f := +lemma convex_on.subset {f : E → β} {t : set E} (h_convex_on 𝕜 : convex_on 𝕜 t f) + (h_subset : s ⊆ t) (h_convex : convex 𝕜 s) : convex_on 𝕜 s f := begin apply and.intro h_convex, intros x y hx hy, exact h_convex_on.2 (h_subset hx) (h_subset hy), end -lemma concave_on.subset {f : E → β} {t : set E} (h_concave_on : concave_on t f) - (h_subset : s ⊆ t) (h_convex : convex ℝ s) : concave_on s f := -@convex_on.subset _ (order_dual β) _ _ _ _ _ f t h_concave_on h_subset h_convex +lemma concave_on.subset {f : E → β} {t : set E} (h_concave_on 𝕜 : concave_on 𝕜 t f) + (h_subset : s ⊆ t) (h_convex : convex 𝕜 s) : concave_on 𝕜 s f := +@convex_on.subset _ (order_dual β) _ _ _ _ _ f t h_concave_on 𝕜 h_subset h_convex -lemma convex_on.add {f g : E → β} (hf : convex_on s f) (hg : convex_on s g) : - convex_on s (λx, f x + g x) := +lemma convex_on.add {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) : + convex_on 𝕜 s (λx, f x + g x) := begin apply and.intro hf.1, intros x y hx hy a b ha hb hab, @@ -256,12 +293,12 @@ begin ... = a • (f x + g x) + b • (f y + g y) : by simp [smul_add, add_assoc] end -lemma concave_on.add {f g : E → β} (hf : concave_on s f) (hg : concave_on s g) : - concave_on s (λx, f x + g x) := +lemma concave_on.add {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) : + concave_on 𝕜 s (λx, f x + g x) := @convex_on.add _ (order_dual β) _ _ _ _ _ f g hf hg -lemma convex_on.smul [ordered_smul ℝ β] {f : E → β} {c : ℝ} (hc : 0 ≤ c) - (hf : convex_on s f) : convex_on s (λx, c • f x) := +lemma convex_on.smul [ordered_smul 𝕜 β] {f : E → β} {c : 𝕜} (hc : 0 ≤ c) + (hf : convex_on 𝕜 s f) : convex_on 𝕜 s (λx, c • f x) := begin apply and.intro hf.1, intros x y hx hy a b ha hb hab, @@ -271,19 +308,19 @@ begin ... = a • (c • f x) + b • (c • f y) : by simp only [smul_add, smul_comm c] end -lemma concave_on.smul [ordered_smul ℝ β] {f : E → β} {c : ℝ} (hc : 0 ≤ c) - (hf : concave_on s f) : concave_on s (λx, c • f x) := +lemma concave_on.smul [ordered_smul 𝕜 β] {f : E → β} {c : 𝕜} (hc : 0 ≤ c) + (hf : concave_on 𝕜 s f) : concave_on 𝕜 s (λx, c • f x) := @convex_on.smul _ (order_dual β) _ _ _ _ _ _ f c hc hf section linear_order section monoid -variables {γ : Type*} [linear_ordered_add_comm_monoid γ] [module ℝ γ] [ordered_smul ℝ γ] +variables {γ : Type*} [linear_ordered_add_comm_monoid γ] [module 𝕜 γ] [ordered_smul 𝕜 γ] {f g : E → γ} /-- The pointwise maximum of convex functions is convex. -/ -lemma convex_on.sup (hf : convex_on s f) (hg : convex_on s g) : - convex_on s (f ⊔ g) := +lemma convex_on.sup (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) : + convex_on 𝕜 s (f ⊔ g) := begin refine ⟨hf.left, λ x y hx hy a b ha hb hab, sup_le _ _⟩, { calc f (a • x + b • y) ≤ a • f x + b • f y : hf.right hx hy ha hb hab @@ -297,12 +334,12 @@ begin end /-- The pointwise minimum of concave functions is concave. -/ -lemma concave_on.inf (hf : concave_on s f) (hg : concave_on s g) : - concave_on s (f ⊓ g) := +lemma concave_on.inf (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) : + concave_on 𝕜 s (f ⊓ g) := @convex_on.sup _ _ _ _ (order_dual γ) _ _ _ _ _ hf hg /-- A convex function on a segment is upper-bounded by the max of its endpoints. -/ -lemma convex_on.le_on_segment' (hf : convex_on s f) {x y : E} {a b : ℝ} +lemma convex_on.le_on_segment' (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f (a • x + b • y) ≤ max (f x) (f y) := calc @@ -313,30 +350,30 @@ calc ... = max (f x) (f y) : by rw [←add_smul, hab, one_smul] /-- A concave function on a segment is lower-bounded by the min of its endpoints. -/ -lemma concave_on.le_on_segment' (hf : concave_on s f) {x y : E} {a b : ℝ} +lemma concave_on.le_on_segment' (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : min (f x) (f y) ≤ f (a • x + b • y) := @convex_on.le_on_segment' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab /-- A convex function on a segment is upper-bounded by the max of its endpoints. -/ -lemma convex_on.le_on_segment (hf : convex_on s f) {x y z : E} - (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[ℝ] y]) : +lemma convex_on.le_on_segment (hf : convex_on 𝕜 s f) {x y z : E} + (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) : f z ≤ max (f x) (f y) := let ⟨a, b, ha, hb, hab, hz⟩ := hz in hz ▸ hf.le_on_segment' hx hy ha hb hab /-- A concave function on a segment is lower-bounded by the min of its endpoints. -/ -lemma concave_on.le_on_segment {f : E → γ} (hf : concave_on s f) {x y z : E} - (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[ℝ] y]) : +lemma concave_on.le_on_segment {f : E → γ} (hf : concave_on 𝕜 s f) {x y z : E} + (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) : min (f x) (f y) ≤ f z := @convex_on.le_on_segment _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz end monoid -variables {γ : Type*} [linear_ordered_cancel_add_comm_monoid γ] [module ℝ γ] [ordered_smul ℝ γ] +variables {γ : Type*} [linear_ordered_cancel_add_comm_monoid γ] [module 𝕜 γ] [ordered_smul 𝕜 γ] {f : E → γ} -- could be shown without contradiction but yeah -lemma convex_on.le_left_of_right_le' (hf : convex_on s f) {x y : E} {a b : ℝ} +lemma convex_on.le_left_of_right_le' (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : f y ≤ f (a • x + b • y)) : f (a • x + b • y) ≤ f x := @@ -350,13 +387,13 @@ begin ... = f (a • x + b • y) : by rw [←add_smul, hab, one_smul], end -lemma concave_on.left_le_of_le_right' (hf : concave_on s f) {x y : E} {a b : ℝ} +lemma concave_on.left_le_of_le_right' (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : f (a • x + b • y) ≤ f y) : f x ≤ f (a • x + b • y) := @convex_on.le_left_of_right_le' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab hxy -lemma convex_on.le_right_of_left_le' (hf : convex_on s f) {x y : E} {a b : ℝ} +lemma convex_on.le_right_of_left_le' (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hxy : f x ≤ f (a • x + b • y)) : f (a • x + b • y) ≤ f y := @@ -365,42 +402,42 @@ begin exact hf.le_left_of_right_le' hy hx hb ha hab hxy, end -lemma concave_on.le_right_of_left_le' (hf : concave_on s f) {x y : E} {a b : ℝ} +lemma concave_on.le_right_of_left_le' (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hxy : f (a • x + b • y) ≤ f x) : f y ≤ f (a • x + b • y) := @convex_on.le_right_of_left_le' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab hxy -lemma convex_on.le_left_of_right_le (hf : convex_on s f) {x y z : E} (hx : x ∈ s) - (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hyz : f y ≤ f z) : +lemma convex_on.le_left_of_right_le (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) + (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f y ≤ f z) : f z ≤ f x := begin obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz, exact hf.le_left_of_right_le' hx hy ha hb.le hab hyz, end -lemma concave_on.left_le_of_le_right (hf : concave_on s f) {x y z : E} (hx : x ∈ s) - (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hyz : f z ≤ f y) : +lemma concave_on.left_le_of_le_right (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) + (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f z ≤ f y) : f x ≤ f z := @convex_on.le_left_of_right_le _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz hyz -lemma convex_on.le_right_of_left_le (hf : convex_on s f) {x y z : E} (hx : x ∈ s) - (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hxz : f x ≤ f z) : +lemma convex_on.le_right_of_left_le (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) + (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f x ≤ f z) : f z ≤ f y := begin obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz, exact hf.le_right_of_left_le' hx hy ha.le hb hab hxz, end -lemma concave_on.le_right_of_left_le (hf : concave_on s f) {x y z : E} (hx : x ∈ s) - (hy : y ∈ s) (hz : z ∈ open_segment ℝ x y) (hxz : f z ≤ f x) : +lemma concave_on.le_right_of_left_le (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) + (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f z ≤ f x) : f y ≤ f z := @convex_on.le_right_of_left_le _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz hxz end linear_order -lemma convex_on.convex_le [ordered_smul ℝ β] {f : E → β} (hf : convex_on s f) (r : β) : - convex ℝ {x ∈ s | f x ≤ r} := +lemma convex_on.convex_le [ordered_smul 𝕜 β] {f : E → β} (hf : convex_on 𝕜 s f) (r : β) : + convex 𝕜 {x ∈ s | f x ≤ r} := λ x y hx hy a b ha hb hab, begin refine ⟨hf.1 hx.1 hy.1 ha hb hab, _⟩, @@ -411,13 +448,13 @@ begin ... ≤ r : by simp [←add_smul, hab] end -lemma concave_on.concave_le [ordered_smul ℝ β] {f : E → β} (hf : concave_on s f) (r : β) : - convex ℝ {x ∈ s | r ≤ f x} := +lemma concave_on.concave_le [ordered_smul 𝕜 β] {f : E → β} (hf : concave_on 𝕜 s f) (r : β) : + convex 𝕜 {x ∈ s | r ≤ f x} := @convex_on.convex_le _ (order_dual β) _ _ _ _ _ _ f hf r lemma convex_on.convex_lt {γ : Type*} [ordered_cancel_add_comm_monoid γ] - [module ℝ γ] [ordered_smul ℝ γ] - {f : E → γ} (hf : convex_on s f) (r : γ) : convex ℝ {x ∈ s | f x < r} := + [module 𝕜 γ] [ordered_smul 𝕜 γ] + {f : E → γ} (hf : convex_on 𝕜 s f) (r : γ) : convex 𝕜 {x ∈ s | f x < r} := begin intros a b as bs xa xb hxa hxb hxaxb, refine ⟨hf.1 as.1 bs.1 hxa hxb hxaxb, _⟩, @@ -436,14 +473,14 @@ begin end lemma concave_on.convex_lt {γ : Type*} [ordered_cancel_add_comm_monoid γ] - [module ℝ γ] [ordered_smul ℝ γ] - {f : E → γ} (hf : concave_on s f) (r : γ) : convex ℝ {x ∈ s | r < f x} := + [module 𝕜 γ] [ordered_smul 𝕜 γ] + {f : E → γ} (hf : concave_on 𝕜 s f) (r : γ) : convex 𝕜 {x ∈ s | r < f x} := @convex_on.convex_lt _ _ _ _ (order_dual γ) _ _ _ f hf r lemma convex_on.convex_epigraph {γ : Type*} [ordered_add_comm_group γ] - [module ℝ γ] [ordered_smul ℝ γ] - {f : E → γ} (hf : convex_on s f) : - convex ℝ {p : E × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} := + [module 𝕜 γ] [ordered_smul 𝕜 γ] + {f : E → γ} (hf : convex_on 𝕜 s f) : + convex 𝕜 {p : E × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} := begin rintros ⟨x, r⟩ ⟨y, t⟩ ⟨hx, hr⟩ ⟨hy, ht⟩ a b ha hb hab, refine ⟨hf.1 hx hy ha hb hab, _⟩, @@ -453,15 +490,15 @@ begin end lemma concave_on.convex_hypograph {γ : Type*} [ordered_add_comm_group γ] - [module ℝ γ] [ordered_smul ℝ γ] - {f : E → γ} (hf : concave_on s f) : - convex ℝ {p : E × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} := + [module 𝕜 γ] [ordered_smul 𝕜 γ] + {f : E → γ} (hf : concave_on 𝕜 s f) : + convex 𝕜 {p : E × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} := @convex_on.convex_epigraph _ _ _ _ (order_dual γ) _ _ _ f hf lemma convex_on_iff_convex_epigraph {γ : Type*} [ordered_add_comm_group γ] - [module ℝ γ] [ordered_smul ℝ γ] + [module 𝕜 γ] [ordered_smul 𝕜 γ] {f : E → γ} : - convex_on s f ↔ convex ℝ {p : E × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} := + convex_on 𝕜 s f ↔ convex 𝕜 {p : E × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} := begin refine ⟨convex_on.convex_epigraph, λ h, ⟨_, _⟩⟩, { assume x y hx hy a b ha hb hab, @@ -471,22 +508,22 @@ begin end lemma concave_on_iff_convex_hypograph {γ : Type*} [ordered_add_comm_group γ] - [module ℝ γ] [ordered_smul ℝ γ] + [module 𝕜 γ] [ordered_smul 𝕜 γ] {f : E → γ} : - concave_on s f ↔ convex ℝ {p : E × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} := + concave_on 𝕜 s f ↔ convex 𝕜 {p : E × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} := @convex_on_iff_convex_epigraph _ _ _ _ (order_dual γ) _ _ _ f /- A linear map is convex. -/ -lemma linear_map.convex_on (f : E →ₗ[ℝ] β) {s : set E} (hs : convex ℝ s) : convex_on s f := +lemma linear_map.convex_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : convex_on 𝕜 s f := ⟨hs, λ _ _ _ _ _ _ _ _ _, by rw [f.map_add, f.map_smul, f.map_smul]⟩ /- A linear map is concave. -/ -lemma linear_map.concave_on (f : E →ₗ[ℝ] β) {s : set E} (hs : convex ℝ s) : concave_on s f := +lemma linear_map.concave_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : concave_on 𝕜 s f := ⟨hs, λ _ _ _ _ _ _ _ _ _, by rw [f.map_add, f.map_smul, f.map_smul]⟩ /-- If a function is convex on `s`, it remains convex when precomposed by an affine map. -/ -lemma convex_on.comp_affine_map {f : F → β} (g : E →ᵃ[ℝ] F) {s : set F} - (hf : convex_on s f) : convex_on (g ⁻¹' s) (f ∘ g) := +lemma convex_on.comp_affine_map {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} + (hf : convex_on 𝕜 s f) : convex_on 𝕜 (g ⁻¹' s) (f ∘ g) := begin refine ⟨hf.1.affine_preimage _,_⟩, intros x y xs ys a b ha hb hab, @@ -498,50 +535,50 @@ begin end /-- If a function is concave on `s`, it remains concave when precomposed by an affine map. -/ -lemma concave_on.comp_affine_map {f : F → β} (g : E →ᵃ[ℝ] F) {s : set F} - (hf : concave_on s f) : concave_on (g ⁻¹' s) (f ∘ g) := +lemma concave_on.comp_affine_map {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} + (hf : concave_on 𝕜 s f) : concave_on 𝕜 (g ⁻¹' s) (f ∘ g) := @convex_on.comp_affine_map _ _ (order_dual β) _ _ _ _ _ _ f g s hf /-- If `g` is convex on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`. -/ -lemma convex_on.comp_linear_map {g : F → β} {s : set F} (hg : convex_on s g) (f : E →ₗ[ℝ] F) : - convex_on (f ⁻¹' s) (g ∘ f) := +lemma convex_on.comp_linear_map {g : F → β} {s : set F} (hg : convex_on 𝕜 s g) (f : E →ₗ[𝕜] F) : + convex_on 𝕜 (f ⁻¹' s) (g ∘ f) := hg.comp_affine_map f.to_affine_map /-- If `g` is concave on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`. -/ -lemma concave_on.comp_linear_map {g : F → β} {s : set F} (hg : concave_on s g) (f : E →ₗ[ℝ] F) : - concave_on (f ⁻¹' s) (g ∘ f) := +lemma concave_on.comp_linear_map {g : F → β} {s : set F} (hg : concave_on 𝕜 s g) (f : E →ₗ[𝕜] F) : + concave_on 𝕜 (f ⁻¹' s) (g ∘ f) := hg.comp_affine_map f.to_affine_map /-- If a function is convex on `s`, it remains convex after a translation. -/ -lemma convex_on.translate_right {f : E → β} {s : set E} {a : E} (hf : convex_on s f) : - convex_on ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := -hf.comp_affine_map $ affine_map.const ℝ E a +ᵥ affine_map.id ℝ E +lemma convex_on.translate_right {f : E → β} {s : set E} {a : E} (hf : convex_on 𝕜 s f) : + convex_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := +hf.comp_affine_map $ affine_map.const 𝕜 E a +ᵥ affine_map.id 𝕜 E /-- If a function is concave on `s`, it remains concave after a translation. -/ -lemma concave_on.translate_right {f : E → β} {s : set E} {a : E} (hf : concave_on s f) : - concave_on ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := -hf.comp_affine_map $ affine_map.const ℝ E a +ᵥ affine_map.id ℝ E +lemma concave_on.translate_right {f : E → β} {s : set E} {a : E} (hf : concave_on 𝕜 s f) : + concave_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := +hf.comp_affine_map $ affine_map.const 𝕜 E a +ᵥ affine_map.id 𝕜 E /-- If a function is convex on `s`, it remains convex after a translation. -/ -lemma convex_on.translate_left {f : E → β} {s : set E} {a : E} (hf : convex_on s f) : - convex_on ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := +lemma convex_on.translate_left {f : E → β} {s : set E} {a : E} (hf : convex_on 𝕜 s f) : + convex_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := by simpa only [add_comm] using hf.translate_right /-- If a function is concave on `s`, it remains concave after a translation. -/ -lemma concave_on.translate_left {f : E → β} {s : set E} {a : E} (hf : concave_on s f) : - concave_on ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := +lemma concave_on.translate_left {f : E → β} {s : set E} {a : E} (hf : concave_on 𝕜 s f) : + concave_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := by simpa only [add_comm] using hf.translate_right /-! ### Jensen's inequality -/ -variables {i j : ι} {c : ℝ} {t : finset ι} {w : ι → ℝ} {p : ι → E} +variables {i j : ι} {c : 𝕜} {t : finset ι} {w : ι → 𝕜} {p : ι → E} /-- Convex **Jensen's inequality**, `finset.linear_combination` version. -/ -lemma convex_on.map_linear_combination_le {f : E → ℝ} (hf : convex_on s f) +lemma convex_on.map_linear_combination_le {f : E → 𝕜} (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (t.linear_combination p w) ≤ t.linear_combination (f ∘ p) w := begin - have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}, + have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × 𝕜 | p.1 ∈ s ∧ f p.1 ≤ p.2}, from λ i hi, ⟨hmem i hi, le_rfl⟩, convert (hf.convex_epigraph.linear_combination_mem h₀ h₁ hmem').2; simp only [linear_combination, function.comp, prod.smul_fst, prod.fst_sum, @@ -549,7 +586,7 @@ begin end /-- Convex **Jensen's inequality**, `finset.sum` version. -/ -lemma convex_on.map_sum_le {f : E → ℝ} (hf : convex_on s f) +lemma convex_on.map_sum_le {f : E → 𝕜} (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i in t, w i • p i) ≤ ∑ i in t, w i * (f (p i)) := by simpa only [linear_combination, h₁, inv_one, one_smul] @@ -559,7 +596,7 @@ by simpa only [linear_combination, h₁, inv_one, one_smul] /-- If a function `f` is convex on `s` takes value `y` at the center of mass of some points `p i ∈ s`, then for some `i` we have `y ≤ f (p i)`. -/ -lemma convex_on.exists_ge_of_linear_combination {f : E → ℝ} (h : convex_on s f) +lemma convex_on.exists_ge_of_linear_combination {f : E → 𝕜} (h : convex_on 𝕜 s f) (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, p i ∈ s) : ∃ i ∈ t, f (t.linear_combination p w) ≤ f (p i) := begin @@ -569,7 +606,7 @@ begin rw mem_filter at hi, exact ⟨i, hi.1, (smul_le_smul_iff_of_pos $ (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩ }, refine exists_le_of_sum_le _ _, - { have := @zero_ne_one ℝ _ _, + { have := @zero_ne_one 𝕜 _ _, rw [←hw₁, ←sum_filter_ne_zero] at this, exact nonempty_of_sum_ne_zero this.symm }, { rw [←linear_combination, ←linear_combination, finset.linear_combination_filter_ne_zero, @@ -578,13 +615,13 @@ begin end /-- Maximum principle for convex functions. If a function `f` is convex on the convex hull of `s`, -then `f` reaches a maximum on `convex_hull ℝ s` outside of `s`. -/ -lemma convex_on.exists_ge_of_mem_convex_hull {f : E → ℝ} (hf : convex_on (convex_hull ℝ s) f) - {x} (hx : x ∈ convex_hull ℝ s) : ∃ y ∈ s, f x ≤ f y := +then `f` reaches a maximum on `convex_hull 𝕜 s` outside of `s`. -/ +lemma convex_on.exists_ge_of_mem_convex_hull {f : E → 𝕜} (hf : convex_on 𝕜 (convex_hull 𝕜 s) f) + {x} (hx : x ∈ convex_hull 𝕜 s) : ∃ y ∈ s, f x ≤ f y := begin rw convex_hull_eq at hx, obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx, rcases hf.exists_ge_of_linear_combination hw₀ hw₁ - (λ i hi, subset_convex_hull ℝ s (hp i hi)) with ⟨i, hit, Hi⟩, + (λ i hi, subset_convex_hull 𝕜 s (hp i hi)) with ⟨i, hit, Hi⟩, exact ⟨p i, hp i hit, Hi⟩ end From 7f5ccd4205f4716ea397d9452c09f25575f17684 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Thu, 23 Sep 2021 15:59:50 +0200 Subject: [PATCH 10/17] done with the API --- src/analysis/calculus/mean_value.lean | 2 +- src/analysis/convex/combination.lean | 13 +- src/analysis/convex/function.lean | 795 ++++++++++++++------------ src/analysis/convex/integral.lean | 13 +- 4 files changed, 445 insertions(+), 378 deletions(-) diff --git a/src/analysis/calculus/mean_value.lean b/src/analysis/calculus/mean_value.lean index d3a16f9eaa4e8..dbf910b1fa619 100644 --- a/src/analysis/calculus/mean_value.lean +++ b/src/analysis/calculus/mean_value.lean @@ -974,7 +974,7 @@ theorem convex_on_of_deriv_mono {D : set ℝ} (hD : convex ℝ D) {f : ℝ → (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f x ≤ deriv f y) : convex_on D f := -convex_on_real_of_slope_mono_adjacent hD +convex_on_of_slope_mono_adjacent hD begin intros x y z hx hz hxy hyz, -- First we prove some trivial inclusions diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index c62ef2c991974..254b95093721e 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -135,10 +135,21 @@ section linear_ordered_field variables {𝕜 E ι ι' : Type*} [linear_ordered_field 𝕜] [add_comm_monoid E] [module 𝕜 E] {s : set E} {t : finset ι} {p : ι → E} {w : ι → 𝕜} -lemma linear_combination_normalize (hw : ∑ i in t, w i ≠ 0) : +lemma linear_combination_normalize (hw : ∑ i in t, w i ≠ 0) : t.linear_combination p w = (∑ i in t, w i) • t.linear_combination p ((∑ i in t, w i)⁻¹ • w) := by rw [linear_combination_smul_right, smul_inv_smul' hw] +lemma linear_combination_normalize_weight_sum (hw : ∑ i in t, w i ≠ 0) : + ∑ i in t, ((∑ i in t, w i)⁻¹ • w) i = 1 := +by { simp_rw pi.smul_apply, rw [←smul_sum, smul_eq_mul, inv_mul_cancel hw] } + +lemma linear_combination_normalize_weight_nonneg (hw : ∀ i ∈ t, 0 ≤ w i) (i : ι) (hi : i ∈ t) : + (0 : 𝕜) ≤ ((∑ i in t, w i)⁻¹ • w) i := +begin + rw [pi.smul_apply, smul_eq_mul], + exact mul_nonneg (inv_nonneg.2 $ sum_nonneg hw) (hw i hi), +end + /-- The linear combination of a finite subset of a convex set belongs to the set provided that all weights are non-negative, and the total weight is `1`. -/ lemma _root_.convex.linear_combination_mem (hs : convex 𝕜 s) : diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index e34b897015d0e..fb521e6d13845 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -26,13 +26,13 @@ a convex set. open finset linear_map set open_locale big_operators classical convex pointwise -variables (𝕜 : Type*) {E F ι ι' β : Type*} +variables {𝕜 E F β ι : Type*} section ordered_semiring -variables [ordered_semiring 𝕜] [add_comm_monoid E] +variables [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] section ordered_add_comm_monoid -variables [ordered_add_comm_monoid β] +variables (𝕜) [ordered_add_comm_monoid β] /-- Convexity of functions -/ def convex_on [has_scalar 𝕜 E] [has_scalar 𝕜 β] (s : set E) (f : E → β) : Prop := @@ -46,17 +46,46 @@ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y) +variables {𝕜} + section has_scalar -variables {𝕜} [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} +variables [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} lemma convex_on_id {s : set 𝕜} (hs : convex 𝕜 s) : convex_on 𝕜 s id := ⟨hs, by { intros, refl }⟩ lemma concave_on_id {s : set 𝕜} (hs : convex 𝕜 s) : concave_on 𝕜 s id := ⟨hs, by { intros, refl }⟩ +lemma convex_on.subset {f : E → β} {t : set E} (hf : convex_on 𝕜 t f) (hst : s ⊆ t) + (hs : convex 𝕜 s) : convex_on 𝕜 s f := +⟨hs, λ x y hx hy, hf.2 (hst hx) (hst hy)⟩ + +lemma concave_on.subset {f : E → β} {t : set E} (hf : concave_on 𝕜 t f) (hst : s ⊆ t) +(hs : convex 𝕜 s) : concave_on 𝕜 s f := +⟨hs, λ x y hx hy, hf.2 (hst hx) (hst hy)⟩ + end has_scalar +section distrib_mul_action +variables [has_scalar 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} + +lemma convex_on.add {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) : + convex_on 𝕜 s (λ x, f x + g x) := +⟨hf.1, λ x y hx hy a b ha hb hab, + calc + f (a • x + b • y) + g (a • x + b • y) ≤ (a • f x + b • f y) + (a • g x + b • g y) + : add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab) + ... = a • f x + a • g x + b • f y + b • g y : by abel + ... = a • (f x + g x) + b • (f y + g y) : by simp only [smul_add, add_assoc]⟩ + +lemma concave_on.add {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) : + concave_on 𝕜 s (λ x, f x + g x) := +@convex_on.add _ _ (order_dual β) _ _ _ _ _ _ f g hf hg + +end distrib_mul_action + section module -variables {𝕜} [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} +variables [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} + lemma convex_on_const (c : β) (hs : convex 𝕜 s) : convex_on 𝕜 s (λ x:E, c) := ⟨hs, λ x y _ _ a b _ _ hab, (convex.combo_self hab c).ge⟩ @@ -65,19 +94,95 @@ lemma concave_on_const (c : β) (hs : convex 𝕜 s) : concave_on 𝕜 s (λ x:E end module +section ordered_smul +variables [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} + +lemma convex_on.convex_le (hf : convex_on 𝕜 s f) (r : β) : + convex 𝕜 {x ∈ s | f x ≤ r} := +λ x y hx hy a b ha hb hab, ⟨hf.1 hx.1 hy.1 ha hb hab, + calc + f (a • x + b • y) ≤ a • (f x) + b • (f y) : hf.2 hx.1 hy.1 ha hb hab + ... ≤ a • r + b • r : add_le_add (smul_le_smul_of_nonneg hx.2 ha) + (smul_le_smul_of_nonneg hy.2 hb) + ... = r : convex.combo_self hab r⟩ + +lemma concave_on.concave_le (hf : concave_on 𝕜 s f) (r : β) : + convex 𝕜 {x ∈ s | r ≤ f x} := +@convex_on.convex_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf r + +lemma convex_on.convex_epigraph (hf : convex_on 𝕜 s f) : + convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} := +begin + rintro ⟨x, r⟩ ⟨y, t⟩ ⟨hx, hr⟩ ⟨hy, ht⟩ a b ha hb hab, + refine ⟨hf.1 hx hy ha hb hab, _⟩, + calc f (a • x + b • y) ≤ a • f x + b • f y : hf.2 hx hy ha hb hab + ... ≤ a • r + b • t : add_le_add (smul_le_smul_of_nonneg hr ha) + (smul_le_smul_of_nonneg ht hb) +end + +lemma concave_on.convex_hypograph (hf : concave_on 𝕜 s f) : + convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1} := +@convex_on.convex_epigraph 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf + +lemma convex_on_iff_convex_epigraph : + convex_on 𝕜 s f ↔ convex 𝕜 {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} := +⟨convex_on.convex_epigraph, λ h, + ⟨λ x y hx hy a b ha hb hab, (@h (x, f x) (y, f y) ⟨hx, le_rfl⟩ ⟨hy, le_rfl⟩ a b ha hb hab).1, + λ x y hx hy a b ha hb hab, (@h (x, f x) (y, f y) ⟨hx, le_rfl⟩ ⟨hy, le_rfl⟩ a b ha hb hab).2⟩⟩ + +lemma concave_on_iff_convex_hypograph : + concave_on 𝕜 s f ↔ convex 𝕜 {p : E × β | p.1 ∈ s ∧ p.2 ≤ f p.1} := +@convex_on_iff_convex_epigraph 𝕜 E (order_dual β) _ _ _ _ _ _ _ f + +end ordered_smul + section module -variables {𝕜} [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} +variables [module 𝕜 E] [module 𝕜 β] -/-- For a function on a convex set in a linear ordered space, in order to prove that it is convex -it suffices to verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` -and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with -lexicographic order. -/ +/-- A linear map is convex. -/ +lemma linear_map.convex_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : convex_on 𝕜 s f := +⟨hs, λ _ _ _ _ _ _ _ _ _, by rw [f.map_add, f.map_smul, f.map_smul]⟩ + +/-- A linear map is concave. -/ +lemma linear_map.concave_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : concave_on 𝕜 s f := +⟨hs, λ _ _ _ _ _ _ _ _ _, by rw [f.map_add, f.map_smul, f.map_smul]⟩ + +/-- If a function is convex on `s`, it remains convex after a translation. -/ +lemma convex_on.translate_right {f : E → β} {s : set E} {c : E} (hf : convex_on 𝕜 s f) : + convex_on 𝕜 ((λ z, c + z) ⁻¹' s) (f ∘ (λ z, c + z)) := +⟨hf.1.translate_preimage_right _, λ x y hx hy a b ha hb hab, + calc + f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y)) + : by rw [smul_add, smul_add, add_add_add_comm, convex.combo_self hab] + ... ≤ a • f (c + x) + b • f (c + y) : hf.2 hx hy ha hb hab⟩ + +/-- If a function is concave on `s`, it remains concave after a translation. -/ +lemma concave_on.translate_right {f : E → β} {s : set E} {a : E} (hf : concave_on 𝕜 s f) : + concave_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := +@convex_on.translate_right 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ hf + +/-- If a function is convex on `s`, it remains convex after a translation. -/ +lemma convex_on.translate_left {f : E → β} {s : set E} {a : E} (hf : convex_on 𝕜 s f) : + convex_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := +by simpa only [add_comm] using hf.translate_right + +/-- If a function is concave on `s`, it remains concave after a translation. -/ +lemma concave_on.translate_left {f : E → β} {s : set E} {a : E} (hf : concave_on 𝕜 s f) : + concave_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := +by simpa only [add_comm] using hf.translate_right + +variables [linear_order E] {s : set E} {f : E → β} + +/-- For a function on a convex set in a linear ordered space (where the order and the algebraic +structures aren't necessarily compatible), in order to prove that it is convex, it suffices to +verify the inequality `f (a • x + b • y) ≤ a • f x + b • f y` only for `x < y` and positive `a`, +`b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order. +-/ lemma linear_order.convex_on_of_lt (hs : convex 𝕜 s) (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) : convex_on 𝕜 s f := begin - use hs, - intros x y hx hy a b ha hb hab, + refine ⟨hs, λ x y hx hy a b ha hb hab, _⟩, wlog hxy : x ≤ y using [x y a b, y x b a], { exact le_total _ _ }, obtain rfl | hxy := hxy.eq_or_lt, @@ -85,238 +190,71 @@ begin obtain rfl | ha' := ha.eq_or_lt, { rw [zero_add] at hab, subst b, simp_rw [zero_smul, zero_add, one_smul] }, obtain rfl | hb' := hb.eq_or_lt, - { rw [add_zero] at hab, subst a }, + { rw [add_zero] at hab, subst a, simp_rw [zero_smul, add_zero, one_smul] }, exact hf hx hy hxy ha' hb' hab, end /-- For a function on a convex set in a linear ordered space, in order to prove that it is concave it suffices to verify the inequality `a • f x + b • f y ≤ f (a • x + b • y)` only for `x < y` -and positive `a`, `b`. The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with +and positive `a`, `b`. The main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with lexicographic order. -/ lemma linear_order.concave_on_of_lt (hs : convex 𝕜 s) (hf : ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)) : concave_on 𝕜 s f := -@linear_order.convex_on_of_lt _ _ (order_dual β) _ _ _ _ _ f _ hs hf +@linear_order.convex_on_of_lt _ _ (order_dual β) _ _ _ _ _ _ s f hs hf end module -end ordered_add_comm_monoid - -section ordered_add_comm_group -variables [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] - -section -variables {𝕜} - -/-- A function `-f` is convex iff `f` is concave. -/ -@[simp] lemma neg_concave_on_iff - (s : set E) (f : E → β) : convex_on 𝕜 s (-f) ↔ concave_on 𝕜 s f := -begin - split, - { rintro ⟨hconv, h⟩, - refine ⟨hconv, _⟩, - intros x y xs ys a b ha hb hab, - specialize h xs ys ha hb hab, - simp [neg_apply, neg_le, add_comm] at h, - exact h }, - { rintro ⟨hconv, h⟩, - refine ⟨hconv, _⟩, - intros x y xs ys a b ha hb hab, - specialize h xs ys ha hb hab, - simp [neg_apply, neg_le, add_comm, h] } -end - -/-- A function `-f` is concave iff `f` is convex. -/ -@[simp] lemma neg_convex_on_iff {γ : Type*} [ordered_add_comm_group γ] [module 𝕜 γ] - (s : set E) (f : E → γ) : concave_on 𝕜 s (-f) ↔ convex_on 𝕜 s f:= -by rw [← neg_concave_on_iff s (-f), neg_neg f] - -end - -end ordered_add_comm_group - -end ordered_semiring - -section linear_ordered_field -variables {𝕜} [linear_ordered_field 𝕜] [add_comm_monoid E] - -section ordered_add_comm_monoid -variables [ordered_add_comm_monoid β] - -section has_scalar -variables [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} - -lemma convex_on_iff_div {f : E → β} : - convex_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b - → f ((a/(a+b)) • x + (b/(a+b)) • y) ≤ (a/(a+b)) • f x + (b/(a+b)) • f y := -and_congr iff.rfl -⟨begin - intros h x y hx hy a b ha hb hab, - apply h hx hy (div_nonneg ha $ le_of_lt hab) (div_nonneg hb $ le_of_lt hab), - rw [←add_div], - exact div_self (ne_of_gt hab) -end, -begin - intros h x y hx hy a b ha hb hab, - simpa [hab, zero_lt_one] using h hx hy ha hb, -end⟩ - -lemma concave_on_iff_div {f : E → β} : - concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b - → (a/(a+b)) • f x + (b/(a+b)) • f y ≤ f ((a/(a+b)) • x + (b/(a+b)) • y) := -@convex_on_iff_div _ _ (order_dual β) _ _ _ _ _ _ _ - -/-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` -the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope -of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity -of a function is used in the proof of convexity of a function with a monotone derivative. -/ -lemma convex_on_real_of_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} - (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → - (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) : - convex_on 𝕜 s f := -linear_order.convex_on_of_lt hs -begin - assume x z hx hz hxz a b ha hb hab, - let y := a * x + b * z, - have hxy : x < y, - { rw [← one_mul x, ← hab, add_mul], - exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _ }, - have hyz : y < z, - { rw [← one_mul z, ← hab, add_mul], - exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _ }, - have : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x), - from (div_le_div_iff (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz), - have A : z - y + (y - x) = z - x, by abel, - have B : 0 < z - x, from sub_pos.2 (lt_trans hxy hyz), - rw [sub_mul, sub_mul, sub_le_iff_le_add', ← add_sub_assoc, le_sub_iff_add_le, ← mul_add, A, - ← le_div_iff B, add_div, mul_div_assoc, mul_div_assoc, - mul_comm (f x), mul_comm (f z)] at this, - rw [eq_comm, ← sub_eq_iff_eq_add] at hab; subst a, - convert this; symmetry; simp only [div_eq_iff (ne_of_gt B), y]; ring -end - -/-- For a function `f` defined on a subset `D` of `𝕜`, if `f` is convex on `D`, then for any three -points `x < y < z`, the slope of the secant line of `f` on `[x, y]` is less than or equal to the -slope of the secant line of `f` on `[x, z]`. -/ -lemma convex_on.slope_mono_adjacent {s : set 𝕜} {f : 𝕜 → 𝕜} (hf : convex_on 𝕜 s f) - {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : - (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) := -begin - have h₁ : 0 < y - x := by linarith, - have h₂ : 0 < z - y := by linarith, - have h₃ : 0 < z - x := by linarith, - suffices : f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y), - by { ring_nf at this ⊢, linarith }, - set a := (z - y) / (z - x), - set b := (y - x) / (z - x), - have heqz : a • x + b • z = y, by { field_simp, rw div_eq_iff; [ring, linarith], }, - have key, from - hf.2 hx hz - (show 0 ≤ a, by apply div_nonneg; linarith) - (show 0 ≤ b, by apply div_nonneg; linarith) - (show a + b = 1, by { field_simp, rw div_eq_iff; [ring, linarith], }), - rw heqz at key, - replace key := mul_le_mul_of_nonneg_left key (le_of_lt h₃), - field_simp [ne_of_gt h₁, ne_of_gt h₂, ne_of_gt h₃, mul_comm (z - x) _] at key ⊢, - rw div_le_div_right, - { linarith, }, - { nlinarith, }, -end - -/-- For a function `f` defined on a convex subset `D` of `𝕜`, `f` is convex on `D` iff, for any -three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is less than or equal to -the slope,of the secant line of `f` on `[x, z]`. -/ -lemma convex_on_real_iff_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} : - convex_on 𝕜 s f ↔ - (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → - (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) := -⟨convex_on.slope_mono_adjacent, convex_on_real_of_slope_mono_adjacent hs⟩ +section module +variables [module 𝕜 E] [module 𝕜 F] [has_scalar 𝕜 β] -/-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` -the slope of the secant line of `f` on `[x, y]` is greater than or equal to the slope -of the secant line of `f` on `[x, z]`, then `f` is concave on `D`. -/ -lemma concave_on_real_of_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} - (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → - (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) : concave_on 𝕜 s f := -begin - rw [←neg_convex_on_iff], - apply convex_on_real_of_slope_mono_adjacent hs, - intros x y z xs zs xy yz, - rw [←neg_le_neg_iff, ←neg_div, ←neg_div, neg_sub, neg_sub], - simp only [hf xs zs xy yz, neg_sub_neg, pi.neg_apply], -end +/-- If `g` is convex on `s`, so is `(f ∘ g)` on `f ⁻¹' s` for a linear `f`. -/ +lemma convex_on.comp_linear_map {f : F → β} {s : set F} (hf : convex_on 𝕜 s f) (g : E →ₗ[𝕜] F) : + convex_on 𝕜 (g ⁻¹' s) (f ∘ g) := +⟨hf.1.linear_preimage _, λ x y hx hy a b ha hb hab, + calc + f (g (a • x + b • y)) = f (a • (g x) + b • (g y)) : by rw [g.map_add, g.map_smul, g.map_smul] + ... ≤ a • f (g x) + b • f (g y) : hf.2 hx hy ha hb hab⟩ -/-- For a function `f` defined on a subset `D` of `𝕜`, if `f` is concave on `D`, then for any three -points `x < y < z`, the slope of the secant line of `f` on `[x, y]` is greater than or equal to the -slope of the secant line of `f` on `[x, z]`. -/ -lemma concave_on.slope_mono_adjacent {s : set 𝕜} {f : 𝕜 → 𝕜} (hf : concave_on 𝕜 s f) - {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : - (f z - f y) / (z - y) ≤ (f y - f x) / (y - x) := -begin - rw [←neg_le_neg_iff, ←neg_div, ←neg_div, neg_sub, neg_sub], - rw [←neg_sub_neg (f y), ←neg_sub_neg (f z)], - simp_rw [←pi.neg_apply], - rw [←neg_convex_on_iff] at hf, - apply convex_on.slope_mono_adjacent hf; assumption, -end +/-- If `g` is concave on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`. -/ +lemma concave_on.comp_linear_map {f : F → β} {s : set F} (hf : concave_on 𝕜 s f) (g : E →ₗ[𝕜] F) : + concave_on 𝕜 (g ⁻¹' s) (f ∘ g) := +@convex_on.comp_linear_map 𝕜 E F (order_dual β) _ _ _ _ _ _ _ f s hf g -/-- For a function `f` defined on a convex subset `D` of `𝕜`, `f` is concave on `D` iff for any -three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is greater than or equal to -the slope of the secant line of `f` on `[x, z]`. -/ -lemma concave_on_real_iff_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} : - concave_on 𝕜 s f ↔ - (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → - (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) := -⟨concave_on.slope_mono_adjacent, concave_on_real_of_slope_mono_adjacent hs⟩ +end module +end ordered_add_comm_monoid -lemma convex_on.subset {f : E → β} {t : set E} (h_convex_on 𝕜 : convex_on 𝕜 t f) - (h_subset : s ⊆ t) (h_convex : convex 𝕜 s) : convex_on 𝕜 s f := -begin - apply and.intro h_convex, - intros x y hx hy, - exact h_convex_on.2 (h_subset hx) (h_subset hy), -end +section ordered_cancel_add_comm_monoid +variables [ordered_cancel_add_comm_monoid β] -lemma concave_on.subset {f : E → β} {t : set E} (h_concave_on 𝕜 : concave_on 𝕜 t f) - (h_subset : s ⊆ t) (h_convex : convex 𝕜 s) : concave_on 𝕜 s f := -@convex_on.subset _ (order_dual β) _ _ _ _ _ f t h_concave_on 𝕜 h_subset h_convex +section module +variables [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} -lemma convex_on.add {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) : - convex_on 𝕜 s (λx, f x + g x) := +lemma convex_on.convex_lt (hf : convex_on 𝕜 s f) (r : β) : convex 𝕜 {x ∈ s | f x < r} := begin - apply and.intro hf.1, - intros x y hx hy a b ha hb hab, - calc - f (a • x + b • y) + g (a • x + b • y) ≤ (a • f x + b • f y) + (a • g x + b • g y) - : add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab) - ... = a • f x + a • g x + b • f y + b • g y : by abel - ... = a • (f x + g x) + b • (f y + g y) : by simp [smul_add, add_assoc] + refine λ x y hx hy a b ha hb hab, ⟨hf.1 hx.1 hy.1 ha hb hab, _⟩, + obtain rfl | ha' := ha.eq_or_lt, + { rw zero_add at hab, + rw [hab, zero_smul, one_smul, zero_add], + exact hy.2 }, + { calc + f (a • x + b • y) + ≤ a • f x + b • f y : hf.2 hx.1 hy.1 ha hb hab + ... < a • r + b • r : add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hx.2 ha') + (smul_le_smul_of_nonneg hy.2.le hb) + ... = r : convex.combo_self hab _ } end -lemma concave_on.add {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) : - concave_on 𝕜 s (λx, f x + g x) := -@convex_on.add _ (order_dual β) _ _ _ _ _ f g hf hg - -lemma convex_on.smul [ordered_smul 𝕜 β] {f : E → β} {c : 𝕜} (hc : 0 ≤ c) - (hf : convex_on 𝕜 s f) : convex_on 𝕜 s (λx, c • f x) := -begin - apply and.intro hf.1, - intros x y hx hy a b ha hb hab, - calc - c • f (a • x + b • y) ≤ c • (a • f x + b • f y) - : smul_le_smul_of_nonneg (hf.2 hx hy ha hb hab) hc - ... = a • (c • f x) + b • (c • f y) : by simp only [smul_add, smul_comm c] -end +lemma concave_on.convex_lt (hf : concave_on 𝕜 s f) (r : β) : convex 𝕜 {x ∈ s | r < f x} := +@convex_on.convex_lt 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf r -lemma concave_on.smul [ordered_smul 𝕜 β] {f : E → β} {c : 𝕜} (hc : 0 ≤ c) - (hf : concave_on 𝕜 s f) : concave_on 𝕜 s (λx, c • f x) := -@convex_on.smul _ (order_dual β) _ _ _ _ _ _ f c hc hf +end module -section linear_order -section monoid +end ordered_cancel_add_comm_monoid -variables {γ : Type*} [linear_ordered_add_comm_monoid γ] [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f g : E → γ} +section linear_ordered_add_comm_monoid +variables [linear_ordered_add_comm_monoid β] [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] + {s : set E} {f g : E → β} /-- The pointwise maximum of convex functions is convex. -/ lemma convex_on.sup (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) : @@ -336,11 +274,11 @@ end /-- The pointwise minimum of concave functions is concave. -/ lemma concave_on.inf (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) : concave_on 𝕜 s (f ⊓ g) := -@convex_on.sup _ _ _ _ (order_dual γ) _ _ _ _ _ hf hg +@convex_on.sup 𝕜 E (order_dual β) _ _ _ _ _ _ _ f g hf hg /-- A convex function on a segment is upper-bounded by the max of its endpoints. -/ -lemma convex_on.le_on_segment' (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} - (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : +lemma convex_on.le_on_segment' (hf : convex_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) + {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f (a • x + b • y) ≤ max (f x) (f y) := calc f (a • x + b • y) ≤ a • f x + b • f y : hf.2 hx hy ha hb hab @@ -350,48 +288,46 @@ calc ... = max (f x) (f y) : by rw [←add_smul, hab, one_smul] /-- A concave function on a segment is lower-bounded by the min of its endpoints. -/ -lemma concave_on.le_on_segment' (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} - (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : +lemma concave_on.le_on_segment' (hf : concave_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) + {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : min (f x) (f y) ≤ f (a • x + b • y) := -@convex_on.le_on_segment' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab +@convex_on.le_on_segment' 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf x y hx hy a b ha hb hab /-- A convex function on a segment is upper-bounded by the max of its endpoints. -/ -lemma convex_on.le_on_segment (hf : convex_on 𝕜 s f) {x y z : E} - (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) : +lemma convex_on.le_on_segment (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) + (hz : z ∈ [x -[𝕜] y]) : f z ≤ max (f x) (f y) := let ⟨a, b, ha, hb, hab, hz⟩ := hz in hz ▸ hf.le_on_segment' hx hy ha hb hab /-- A concave function on a segment is lower-bounded by the min of its endpoints. -/ -lemma concave_on.le_on_segment {f : E → γ} (hf : concave_on 𝕜 s f) {x y z : E} - (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) : - min (f x) (f y) ≤ f z := -@convex_on.le_on_segment _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz +lemma concave_on.le_on_segment (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) + (hz : z ∈ [x -[𝕜] y]) : + min (f x) (f y) ≤ f z := +@convex_on.le_on_segment 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf x y z hx hy hz + +end linear_ordered_add_comm_monoid -end monoid +section linear_ordered_cancel_add_comm_monoid +variables [linear_ordered_cancel_add_comm_monoid β] -variables {γ : Type*} [linear_ordered_cancel_add_comm_monoid γ] [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} +section ordered_smul +variables [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} --- could be shown without contradiction but yeah -lemma convex_on.le_left_of_right_le' (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} - (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) - (hxy : f y ≤ f (a • x + b • y)) : +lemma convex_on.le_left_of_right_le' (hf : convex_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) + {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : f y ≤ f (a • x + b • y)) : f (a • x + b • y) ≤ f x := -begin - apply le_of_not_lt (λ h, lt_irrefl (f (a • x + b • y)) _), +le_of_not_lt $ λ h, lt_irrefl (f (a • x + b • y)) $ calc f (a • x + b • y) ≤ a • f x + b • f y : hf.2 hx hy ha.le hb hab ... < a • f (a • x + b • y) + b • f (a • x + b • y) : add_lt_add_of_lt_of_le (smul_lt_smul_of_pos h ha) (smul_le_smul_of_nonneg hxy hb) - ... = f (a • x + b • y) : by rw [←add_smul, hab, one_smul], -end + ... = f (a • x + b • y) : by rw [←add_smul, hab, one_smul] -lemma concave_on.left_le_of_le_right' (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} - (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) - (hxy : f (a • x + b • y) ≤ f y) : +lemma concave_on.left_le_of_le_right' (hf : concave_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) + {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hxy : f (a • x + b • y) ≤ f y) : f x ≤ f (a • x + b • y) := -@convex_on.le_left_of_right_le' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab hxy +@convex_on.le_left_of_right_le' 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf x y hx hy a b ha hb hab hxy lemma convex_on.le_right_of_left_le' (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) @@ -406,7 +342,7 @@ lemma concave_on.le_right_of_left_le' (hf : concave_on 𝕜 s f) {x y : E} {a b (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hxy : f (a • x + b • y) ≤ f x) : f y ≤ f (a • x + b • y) := -@convex_on.le_right_of_left_le' _ _ _ _ (order_dual γ) _ _ _ f hf x y a b hx hy ha hb hab hxy +@convex_on.le_right_of_left_le' 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf x y a b hx hy ha hb hab hxy lemma convex_on.le_left_of_right_le (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f y ≤ f z) : @@ -419,7 +355,7 @@ end lemma concave_on.left_le_of_le_right (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f z ≤ f y) : f x ≤ f z := -@convex_on.le_left_of_right_le _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz hyz +@convex_on.le_left_of_right_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf x y z hx hy hz hyz lemma convex_on.le_right_of_left_le (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f x ≤ f z) : @@ -432,168 +368,285 @@ end lemma concave_on.le_right_of_left_le (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f z ≤ f x) : f y ≤ f z := -@convex_on.le_right_of_left_le _ _ _ _ (order_dual γ) _ _ _ f hf x y z hx hy hz hxz +@convex_on.le_right_of_left_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf x y z hx hy hz hxz -end linear_order +end ordered_smul +end linear_ordered_cancel_add_comm_monoid -lemma convex_on.convex_le [ordered_smul 𝕜 β] {f : E → β} (hf : convex_on 𝕜 s f) (r : β) : - convex 𝕜 {x ∈ s | f x ≤ r} := -λ x y hx hy a b ha hb hab, +section ordered_add_comm_group +variables [ordered_add_comm_group β] [has_scalar 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} + +/-- A function `-f` is convex iff `f` is concave. -/ +@[simp] lemma neg_convex_on_iff : + convex_on 𝕜 s (-f) ↔ concave_on 𝕜 s f := begin - refine ⟨hf.1 hx.1 hy.1 ha hb hab, _⟩, - calc - f (a • x + b • y) ≤ a • (f x) + b • (f y) : hf.2 hx.1 hy.1 ha hb hab - ... ≤ a • r + b • r : add_le_add (smul_le_smul_of_nonneg hx.2 ha) - (smul_le_smul_of_nonneg hy.2 hb) - ... ≤ r : by simp [←add_smul, hab] + split, + { rintro ⟨hconv, h⟩, + refine ⟨hconv, λ x y hx hy a b ha hb hab, _⟩, + simp [neg_apply, neg_le, add_comm] at h, + exact h hx hy ha hb hab }, + { rintro ⟨hconv, h⟩, + refine ⟨hconv, λ x y hx hy a b ha hb hab, _⟩, + rw ←neg_le_neg_iff, + simp_rw [neg_add, pi.neg_apply, smul_neg, neg_neg], + exact h hx hy ha hb hab } end -lemma concave_on.concave_le [ordered_smul 𝕜 β] {f : E → β} (hf : concave_on 𝕜 s f) (r : β) : - convex 𝕜 {x ∈ s | r ≤ f x} := -@convex_on.convex_le _ (order_dual β) _ _ _ _ _ _ f hf r +/-- A function `-f` is concave iff `f` is convex. -/ +@[simp] lemma neg_concave_on_iff : concave_on 𝕜 s (-f) ↔ convex_on 𝕜 s f:= +by rw [← neg_convex_on_iff, neg_neg f] -lemma convex_on.convex_lt {γ : Type*} [ordered_cancel_add_comm_monoid γ] - [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} (hf : convex_on 𝕜 s f) (r : γ) : convex 𝕜 {x ∈ s | f x < r} := -begin - intros a b as bs xa xb hxa hxb hxaxb, - refine ⟨hf.1 as.1 bs.1 hxa hxb hxaxb, _⟩, - by_cases H : xa = 0, - { have H' : xb = 1 := by rwa [H, zero_add] at hxaxb, - rw [H, H', zero_smul, one_smul, zero_add], - exact bs.2 }, - { calc - f (xa • a + xb • b) ≤ xa • (f a) + xb • (f b) : hf.2 as.1 bs.1 hxa hxb hxaxb - ... < xa • r + xb • (f b) : (add_lt_add_iff_right (xb • (f b))).mpr - (smul_lt_smul_of_pos as.2 - (lt_of_le_of_ne hxa (ne.symm H))) - ... ≤ xa • r + xb • r : (add_le_add_iff_left (xa • r)).mpr - (smul_le_smul_of_nonneg bs.2.le hxb) - ... = r : by simp only [←add_smul, hxaxb, one_smul] } -end +alias neg_convex_on_iff ↔ _ concave_on.neg +alias neg_concave_on_iff ↔ _ convex_on.neg -lemma concave_on.convex_lt {γ : Type*} [ordered_cancel_add_comm_monoid γ] - [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} (hf : concave_on 𝕜 s f) (r : γ) : convex 𝕜 {x ∈ s | r < f x} := -@convex_on.convex_lt _ _ _ _ (order_dual γ) _ _ _ f hf r +end ordered_add_comm_group +end ordered_semiring -lemma convex_on.convex_epigraph {γ : Type*} [ordered_add_comm_group γ] - [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} (hf : convex_on 𝕜 s f) : - convex 𝕜 {p : E × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} := -begin - rintros ⟨x, r⟩ ⟨y, t⟩ ⟨hx, hr⟩ ⟨hy, ht⟩ a b ha hb hab, - refine ⟨hf.1 hx hy ha hb hab, _⟩, - calc f (a • x + b • y) ≤ a • f x + b • f y : hf.2 hx hy ha hb hab - ... ≤ a • r + b • t : add_le_add (smul_le_smul_of_nonneg hr ha) - (smul_le_smul_of_nonneg ht hb) -end +section ordered_comm_semiring +variables [ordered_comm_semiring 𝕜] [add_comm_monoid E] -lemma concave_on.convex_hypograph {γ : Type*} [ordered_add_comm_group γ] - [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} (hf : concave_on 𝕜 s f) : - convex 𝕜 {p : E × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} := -@convex_on.convex_epigraph _ _ _ _ (order_dual γ) _ _ _ f hf +section ordered_add_comm_monoid +variables [ordered_add_comm_monoid β] -lemma convex_on_iff_convex_epigraph {γ : Type*} [ordered_add_comm_group γ] - [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} : - convex_on 𝕜 s f ↔ convex 𝕜 {p : E × γ | p.1 ∈ s ∧ f p.1 ≤ p.2} := -begin - refine ⟨convex_on.convex_epigraph, λ h, ⟨_, _⟩⟩, - { assume x y hx hy a b ha hb hab, - exact (@h (x, f x) (y, f y) ⟨hx, le_refl _⟩ ⟨hy, le_refl _⟩ a b ha hb hab).1 }, - { assume x y hx hy a b ha hb hab, - exact (@h (x, f x) (y, f y) ⟨hx, le_refl _⟩ ⟨hy, le_refl _⟩ a b ha hb hab).2 } -end +section module +variables [has_scalar 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} -lemma concave_on_iff_convex_hypograph {γ : Type*} [ordered_add_comm_group γ] - [module 𝕜 γ] [ordered_smul 𝕜 γ] - {f : E → γ} : - concave_on 𝕜 s f ↔ convex 𝕜 {p : E × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} := -@convex_on_iff_convex_epigraph _ _ _ _ (order_dual γ) _ _ _ f +lemma convex_on.smul {c : 𝕜} (hc : 0 ≤ c) + (hf : convex_on 𝕜 s f) : convex_on 𝕜 s (λ x, c • f x) := +⟨hf.1, λ x y hx hy a b ha hb hab, + calc + c • f (a • x + b • y) ≤ c • (a • f x + b • f y) + : smul_le_smul_of_nonneg (hf.2 hx hy ha hb hab) hc + ... = a • (c • f x) + b • (c • f y) + : by rw [smul_add, smul_comm c, smul_comm c]; apply_instance⟩ -/- A linear map is convex. -/ -lemma linear_map.convex_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : convex_on 𝕜 s f := -⟨hs, λ _ _ _ _ _ _ _ _ _, by rw [f.map_add, f.map_smul, f.map_smul]⟩ +lemma concave_on.smul {c : 𝕜} (hc : 0 ≤ c) + (hf : concave_on 𝕜 s f) : concave_on 𝕜 s (λ x, c • f x) := +@convex_on.smul _ _ (order_dual β) _ _ _ _ _ _ _ f c hc hf -/- A linear map is concave. -/ -lemma linear_map.concave_on (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) : concave_on 𝕜 s f := -⟨hs, λ _ _ _ _ _ _ _ _ _, by rw [f.map_add, f.map_smul, f.map_smul]⟩ +end module +end ordered_add_comm_monoid +end ordered_comm_semiring + +section ordered_ring +variables [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] + +section ordered_add_comm_monoid +variables [ordered_add_comm_monoid β] + +section module +variables [module 𝕜 E] [module 𝕜 F] [has_scalar 𝕜 β] /-- If a function is convex on `s`, it remains convex when precomposed by an affine map. -/ -lemma convex_on.comp_affine_map {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} - (hf : convex_on 𝕜 s f) : convex_on 𝕜 (g ⁻¹' s) (f ∘ g) := -begin - refine ⟨hf.1.affine_preimage _,_⟩, - intros x y xs ys a b ha hb hab, +lemma convex_on.comp_affine_map {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : convex_on 𝕜 s f) : + convex_on 𝕜 (g ⁻¹' s) (f ∘ g) := +⟨hf.1.affine_preimage _, λ x y hx hy a b ha hb hab, calc (f ∘ g) (a • x + b • y) = f (g (a • x + b • y)) : rfl ... = f (a • (g x) + b • (g y)) : by rw [convex.combo_affine_apply hab] - ... ≤ a • f (g x) + b • f (g y) : hf.2 xs ys ha hb hab - ... = a • (f ∘ g) x + b • (f ∘ g) y : rfl -end + ... ≤ a • f (g x) + b • f (g y) : hf.2 hx hy ha hb hab⟩ /-- If a function is concave on `s`, it remains concave when precomposed by an affine map. -/ -lemma concave_on.comp_affine_map {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} - (hf : concave_on 𝕜 s f) : concave_on 𝕜 (g ⁻¹' s) (f ∘ g) := -@convex_on.comp_affine_map _ _ (order_dual β) _ _ _ _ _ _ f g s hf +lemma concave_on.comp_affine_map {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : concave_on 𝕜 s f) : + concave_on 𝕜 (g ⁻¹' s) (f ∘ g) := +@convex_on.comp_affine_map _ _ _ (order_dual β) _ _ _ _ _ _ _ f g s hf + +end module +end ordered_add_comm_monoid +end ordered_ring + +section linear_ordered_field +variables [linear_ordered_field 𝕜] [add_comm_monoid E] + +section ordered_add_comm_monoid +variables [ordered_add_comm_monoid β] + +section has_scalar +variables [has_scalar 𝕜 E] [has_scalar 𝕜 β] {s : set E} + +lemma convex_on_iff_div {f : E → β} : + convex_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b + → f ((a/(a+b)) • x + (b/(a+b)) • y) ≤ (a/(a+b)) • f x + (b/(a+b)) • f y := +and_congr iff.rfl +⟨begin + intros h x y hx hy a b ha hb hab, + apply h hx hy (div_nonneg ha hab.le) (div_nonneg hb hab.le), + rw [←add_div, div_self hab.ne'], +end, +begin + intros h x y hx hy a b ha hb hab, + simpa [hab, zero_lt_one] using h hx hy ha hb, +end⟩ + +lemma concave_on_iff_div {f : E → β} : + concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b + → (a/(a+b)) • f x + (b/(a+b)) • f y ≤ f ((a/(a+b)) • x + (b/(a+b)) • y) := +@convex_on_iff_div _ _ (order_dual β) _ _ _ _ _ _ _ + +/-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` +the slope of the secant line of `f` on `[x, y]` is less than or equal to the slope +of the secant line of `f` on `[x, z]`, then `f` is convex on `D`. This way of proving convexity +of a function is used in the proof of convexity of a function with a monotone derivative. -/ +lemma convex_on_of_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} + (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → + (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) : + convex_on 𝕜 s f := +linear_order.convex_on_of_lt hs +begin + assume x z hx hz hxz a b ha hb hab, + let y := a * x + b * z, + have hxy : x < y, + { rw [← one_mul x, ← hab, add_mul], + exact add_lt_add_left ((mul_lt_mul_left hb).2 hxz) _ }, + have hyz : y < z, + { rw [← one_mul z, ← hab, add_mul], + exact add_lt_add_right ((mul_lt_mul_left ha).2 hxz) _ }, + have : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x), + from (div_le_div_iff (sub_pos.2 hxy) (sub_pos.2 hyz)).1 (hf hx hz hxy hyz), + have hxz : 0 < z - x, from sub_pos.2 (hxy.trans hyz), + have ha : (z - y) / (z - x) = a, + { rw [eq_comm, ← sub_eq_iff_eq_add'] at hab, + simp_rw [div_eq_iff hxz.ne', y, ←hab], ring }, + have hb : (y - x) / (z - x) = b, + { rw [eq_comm, ← sub_eq_iff_eq_add] at hab, + simp_rw [div_eq_iff hxz.ne', y, ←hab], ring }, + rwa [sub_mul, sub_mul, sub_le_iff_le_add', ← add_sub_assoc, le_sub_iff_add_le, ← mul_add, + sub_add_sub_cancel, ← le_div_iff hxz, add_div, mul_div_assoc, mul_div_assoc, mul_comm (f x), + mul_comm (f z), ha, hb] at this, +end + +/-- For a function `f` defined on a subset `D` of `𝕜`, if `f` is convex on `D`, then for any three +points `x < y < z`, the slope of the secant line of `f` on `[x, y]` is less than or equal to the +slope of the secant line of `f` on `[x, z]`. -/ +lemma convex_on.slope_mono_adjacent {s : set 𝕜} {f : 𝕜 → 𝕜} (hf : convex_on 𝕜 s f) + {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : + (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) := +begin + have h₁ : 0 < y - x := by linarith, + have h₂ : 0 < z - y := by linarith, + have h₃ : 0 < z - x := by linarith, + suffices : f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y), + { ring_nf at this ⊢, linarith }, + set a := (z - y) / (z - x), + set b := (y - x) / (z - x), + have heqz : a • x + b • z = y, by { field_simp, rw div_eq_iff; [ring, linarith] }, + have key, from + hf.2 hx hz + (show 0 ≤ a, by apply div_nonneg; linarith) + (show 0 ≤ b, by apply div_nonneg; linarith) + (show a + b = 1, by { field_simp, rw div_eq_iff; [ring, linarith] }), + rw heqz at key, + replace key := mul_le_mul_of_nonneg_left key h₃.le, + field_simp [h₁.ne', h₂.ne', h₃.ne', mul_comm (z - x) _] at key ⊢, + rw div_le_div_right, + { linarith }, + { nlinarith } +end + +/-- For a function `f` defined on a convex subset `D` of `𝕜`, `f` is convex on `D` iff, for any +three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is less than or equal to +the slope,of the secant line of `f` on `[x, z]`. -/ +lemma convex_on_iff_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} : + convex_on 𝕜 s f ↔ + (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → + (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) := +⟨convex_on.slope_mono_adjacent, convex_on_of_slope_mono_adjacent hs⟩ + +/-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` +the slope of the secant line of `f` on `[x, y]` is greater than or equal to the slope +of the secant line of `f` on `[x, z]`, then `f` is concave on `D`. -/ +lemma concave_on_of_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} + (hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → + (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) : concave_on 𝕜 s f := +begin + rw ←neg_convex_on_iff, + refine convex_on_of_slope_mono_adjacent hs (λ x y z hx hz hxy hyz, _), + rw ←neg_le_neg_iff, + simp_rw [←neg_div, neg_sub, pi.neg_apply, neg_sub_neg], + exact hf hx hz hxy hyz, +end + +/-- For a function `f` defined on a subset `D` of `𝕜`, if `f` is concave on `D`, then for any three +points `x < y < z`, the slope of the secant line of `f` on `[x, y]` is greater than or equal to the +slope of the secant line of `f` on `[x, z]`. -/ +lemma concave_on.slope_mono_adjacent {s : set 𝕜} {f : 𝕜 → 𝕜} (hf : concave_on 𝕜 s f) + {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : + (f z - f y) / (z - y) ≤ (f y - f x) / (y - x) := +begin + rw [←neg_le_neg_iff, ←neg_sub_neg (f x), ←neg_sub_neg (f y)], + simp_rw [←pi.neg_apply, ←neg_div, neg_sub], + exact convex_on.slope_mono_adjacent hf.neg hx hz hxy hyz, +end + +/-- For a function `f` defined on a convex subset `D` of `𝕜`, `f` is concave on `D` iff for any +three points `x < y < z` the slope of the secant line of `f` on `[x, y]` is greater than or equal to +the slope of the secant line of `f` on `[x, z]`. -/ +lemma concave_on_iff_slope_mono_adjacent {s : set 𝕜} (hs : convex 𝕜 s) {f : 𝕜 → 𝕜} : + concave_on 𝕜 s f ↔ + (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → + (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) := +⟨concave_on.slope_mono_adjacent, concave_on_of_slope_mono_adjacent hs⟩ + +end has_scalar +end ordered_add_comm_monoid +end linear_ordered_field -/-- If `g` is convex on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`. -/ -lemma convex_on.comp_linear_map {g : F → β} {s : set F} (hg : convex_on 𝕜 s g) (f : E →ₗ[𝕜] F) : - convex_on 𝕜 (f ⁻¹' s) (g ∘ f) := -hg.comp_affine_map f.to_affine_map -/-- If `g` is concave on `s`, so is `(g ∘ f)` on `f ⁻¹' s` for a linear `f`. -/ -lemma concave_on.comp_linear_map {g : F → β} {s : set F} (hg : concave_on 𝕜 s g) (f : E →ₗ[𝕜] F) : - concave_on 𝕜 (f ⁻¹' s) (g ∘ f) := -hg.comp_affine_map f.to_affine_map -/-- If a function is convex on `s`, it remains convex after a translation. -/ -lemma convex_on.translate_right {f : E → β} {s : set E} {a : E} (hf : convex_on 𝕜 s f) : - convex_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := -hf.comp_affine_map $ affine_map.const 𝕜 E a +ᵥ affine_map.id 𝕜 E -/-- If a function is concave on `s`, it remains concave after a translation. -/ -lemma concave_on.translate_right {f : E → β} {s : set E} {a : E} (hf : concave_on 𝕜 s f) : - concave_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, a + z)) := -hf.comp_affine_map $ affine_map.const 𝕜 E a +ᵥ affine_map.id 𝕜 E -/-- If a function is convex on `s`, it remains convex after a translation. -/ -lemma convex_on.translate_left {f : E → β} {s : set E} {a : E} (hf : convex_on 𝕜 s f) : - convex_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := -by simpa only [add_comm] using hf.translate_right -/-- If a function is concave on `s`, it remains concave after a translation. -/ -lemma concave_on.translate_left {f : E → β} {s : set E} {a : E} (hf : concave_on 𝕜 s f) : - concave_on 𝕜 ((λ z, a + z) ⁻¹' s) (f ∘ (λ z, z + a)) := -by simpa only [add_comm] using hf.translate_right /-! ### Jensen's inequality -/ -variables {i j : ι} {c : 𝕜} {t : finset ι} {w : ι → 𝕜} {p : ι → E} +section jensen +variables [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] + [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {t : finset ι} {w : ι → 𝕜} {p : ι → E} /-- Convex **Jensen's inequality**, `finset.linear_combination` version. -/ -lemma convex_on.map_linear_combination_le {f : E → 𝕜} (hf : convex_on 𝕜 s f) - (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) - (hmem : ∀ i ∈ t, p i ∈ s) : f (t.linear_combination p w) ≤ t.linear_combination (f ∘ p) w := +lemma convex_on.map_linear_combination_le (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) + (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : + f (t.linear_combination p w) ≤ t.linear_combination (f ∘ p) w := begin - have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × 𝕜 | p.1 ∈ s ∧ f p.1 ≤ p.2}, + have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}, from λ i hi, ⟨hmem i hi, le_rfl⟩, convert (hf.convex_epigraph.linear_combination_mem h₀ h₁ hmem').2; simp only [linear_combination, function.comp, prod.smul_fst, prod.fst_sum, - prod.smul_snd, prod.snd_sum] + prod.smul_snd, prod.snd_sum], end +/-- Concave **Jensen's inequality**, `finset.linear_combination` version. -/ +lemma concave_on.le_map_linear_combination (hf : concave_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) + (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : + t.linear_combination (f ∘ p) w ≤ f (t.linear_combination p w) := +@convex_on.map_linear_combination_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ _ _ _ _ hf h₀ h₁ hmem + /-- Convex **Jensen's inequality**, `finset.sum` version. -/ -lemma convex_on.map_sum_le {f : E → 𝕜} (hf : convex_on 𝕜 s f) - (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) - (hmem : ∀ i ∈ t, p i ∈ s) : f (∑ i in t, w i • p i) ≤ ∑ i in t, w i * (f (p i)) := -by simpa only [linear_combination, h₁, inv_one, one_smul] - using hf.map_linear_combination_le h₀ h₁ hmem +lemma convex_on.map_sum_le (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i ≠ 0) + (hmem : ∀ i ∈ t, p i ∈ s) : + f ((∑ i in t, w i)⁻¹ • ∑ i in t, w i • p i) ≤ (∑ i in t, w i)⁻¹ • ∑ i in t, w i • f (p i) := +begin + rw [←linear_combination, ←linear_combination_smul_right, ←linear_combination, + ←linear_combination_smul_right], + exact hf.map_linear_combination_le (linear_combination_normalize_weight_nonneg h₀) + (linear_combination_normalize_weight_sum h₁) hmem, +end + +/-- Concave **Jensen's inequality**, `finset.sum` version. -/ +lemma concave_on.le_map_sum (hf : concave_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i ≠ 0) + (hmem : ∀ i ∈ t, p i ∈ s) : + (∑ i in t, w i)⁻¹ • ∑ i in t, w i • f (p i) ≤ f ((∑ i in t, w i)⁻¹ • ∑ i in t, w i • p i) := +@convex_on.map_sum_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ _ _ _ _ hf h₀ h₁ hmem + +end jensen /-! ### Maximum principle -/ +section maximum_principle +variables [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] + [mul_action_with_zero 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {t : finset ι} {w : ι → 𝕜} + {p : ι → E} + /-- If a function `f` is convex on `s` takes value `y` at the center of mass of some points `p i ∈ s`, then for some `i` we have `y ≤ f (p i)`. -/ lemma convex_on.exists_ge_of_linear_combination {f : E → 𝕜} (h : convex_on 𝕜 s f) @@ -625,3 +678,5 @@ begin (λ i hi, subset_convex_hull 𝕜 s (hp i hi)) with ⟨i, hit, Hi⟩, exact ⟨p i, hp i hit, Hi⟩ end + +end maximum_principle diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index 793bbe5e9e42f..0bee342349f07 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -21,13 +21,14 @@ In this file we prove four theorems: belongs to `s`: `∫ x, f x ∂μ ∈ s`. See also `convex.linear_combination_mem` for a finite sum version of this lemma. -* `convex_on.map_smul_integral_le`: Jensen's inequality: if a function `g : E → ℝ` is convex and - continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is - a function sending `μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is - less than or equal to the average value of `g ∘ f` provided that both `f` and `g ∘ f` are - integrable. See also `convex.map_linear_combination_le` for a finite sum version of this lemma. +* `convex_on.map_smul_integral_le`: Convex Jensen's inequality: If a function `g : E → ℝ` is convex + and continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and + `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the average + value of `f` is less than or equal to the average value of `g ∘ f` provided that both `f` and + `g ∘ f` are integrable. See also `convex_on.map_linear_combination_le` for a finite sum version of + this lemma. -* `convex_on.map_integral_le`: Jensen's inequality: if a function `g : E → ℝ` is convex and +* `convex_on.map_integral_le`: Convex Jensen's inequality: If a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected value of `g ∘ f` provided that both `f` and `g ∘ f` are From 410eb13a3d98b455e6b397e89d2db0fcdbdabfe7 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Thu, 23 Sep 2021 16:14:10 +0200 Subject: [PATCH 11/17] other files --- src/analysis/calculus/mean_value.lean | 23 ++++++++++----------- src/analysis/convex/exposed.lean | 10 ++++----- src/analysis/convex/extrema.lean | 10 ++++----- src/analysis/convex/function.lean | 10 ++++----- src/analysis/convex/integral.lean | 4 ++-- src/analysis/convex/specific_functions.lean | 16 +++++++------- src/analysis/convex/topology.lean | 2 +- 7 files changed, 37 insertions(+), 38 deletions(-) diff --git a/src/analysis/calculus/mean_value.lean b/src/analysis/calculus/mean_value.lean index dbf910b1fa619..bfae9684e62d9 100644 --- a/src/analysis/calculus/mean_value.lean +++ b/src/analysis/calculus/mean_value.lean @@ -973,7 +973,7 @@ and `f'` is monotone on the interior, then `f` is convex on `D`. -/ theorem convex_on_of_deriv_mono {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f x ≤ deriv f y) : - convex_on D f := + convex_on ℝ D f := convex_on_of_slope_mono_adjacent hD begin intros x y z hx hz hxy hyz, @@ -999,25 +999,24 @@ and `f'` is antimonotone on the interior, then `f` is concave on `D`. -/ theorem concave_on_of_deriv_antimono {D : set ℝ} (hD : convex ℝ D) {f : ℝ → ℝ} (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f y ≤ deriv f x) : - concave_on D f := + concave_on ℝ D f := begin have : ∀ x y ∈ interior D, x ≤ y → deriv (-f) x ≤ deriv (-f) y, { intros x y hx hy hxy, convert neg_le_neg (hf'_mono x y hx hy hxy); convert deriv.neg }, - exact (neg_convex_on_iff D f).mp (convex_on_of_deriv_mono hD - hf.neg hf'.neg this), + exact neg_convex_on_iff.mp (convex_on_of_deriv_mono hD hf.neg hf'.neg this), end /-- If a function `f` is differentiable and `f'` is monotone on `ℝ` then `f` is convex. -/ theorem convex_on_univ_of_deriv_mono {f : ℝ → ℝ} (hf : differentiable ℝ f) - (hf'_mono : monotone (deriv f)) : convex_on univ f := + (hf'_mono : monotone (deriv f)) : convex_on ℝ univ f := convex_on_of_deriv_mono convex_univ hf.continuous.continuous_on hf.differentiable_on (λ x y _ _ h, hf'_mono h) /-- If a function `f` is differentiable and `f'` is antimonotone on `ℝ` then `f` is concave. -/ theorem concave_on_univ_of_deriv_antimono {f : ℝ → ℝ} (hf : differentiable ℝ f) - (hf'_antimono : ∀⦃a b⦄, a ≤ b → (deriv f) b ≤ (deriv f) a) : concave_on univ f := + (hf'_antimono : ∀⦃a b⦄, a ≤ b → (deriv f) b ≤ (deriv f) a) : concave_on ℝ univ f := concave_on_of_deriv_antimono convex_univ hf.continuous.continuous_on hf.differentiable_on (λ x y _ _ h, hf'_antimono h) @@ -1027,7 +1026,7 @@ theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex ℝ D) {f : ℝ (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'' : differentiable_on ℝ (deriv f) (interior D)) (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ (deriv^[2] f x)) : - convex_on D f := + convex_on ℝ D f := convex_on_of_deriv_mono hD hf hf' $ assume x y hx hy hxy, hD.interior.mono_of_deriv_nonneg hf''.continuous_on (by rwa [interior_interior]) @@ -1039,7 +1038,7 @@ theorem concave_on_of_deriv2_nonpos {D : set ℝ} (hD : convex ℝ D) {f : ℝ (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D)) (hf'' : differentiable_on ℝ (deriv f) (interior D)) (hf''_nonpos : ∀ x ∈ interior D, (deriv^[2] f x) ≤ 0) : - concave_on D f := + concave_on ℝ D f := concave_on_of_deriv_antimono hD hf hf' $ assume x y hx hy hxy, hD.interior.antimono_of_deriv_nonpos hf''.continuous_on (by rwa [interior_interior]) @@ -1049,7 +1048,7 @@ hD.interior.antimono_of_deriv_nonpos hf''.continuous_on (by rwa [interior_interi `f''` is nonnegative on `D`, then `f` is convex on `D`. -/ theorem convex_on_open_of_deriv2_nonneg {D : set ℝ} (hD : convex ℝ D) (hD₂ : is_open D) {f : ℝ → ℝ} (hf' : differentiable_on ℝ f D) (hf'' : differentiable_on ℝ (deriv f) D) - (hf''_nonneg : ∀ x ∈ D, 0 ≤ (deriv^[2] f x)) : convex_on D f := + (hf''_nonneg : ∀ x ∈ D, 0 ≤ (deriv^[2] f x)) : convex_on ℝ D f := convex_on_of_deriv2_nonneg hD hf'.continuous_on (by simpa [hD₂.interior_eq] using hf') (by simpa [hD₂.interior_eq] using hf'') (by simpa [hD₂.interior_eq] using hf''_nonneg) @@ -1057,7 +1056,7 @@ convex_on_of_deriv2_nonneg hD hf'.continuous_on (by simpa [hD₂.interior_eq] us `f''` is nonpositive on `D`, then `f` is concave on `D`. -/ theorem concave_on_open_of_deriv2_nonpos {D : set ℝ} (hD : convex ℝ D) (hD₂ : is_open D) {f : ℝ → ℝ} (hf' : differentiable_on ℝ f D) (hf'' : differentiable_on ℝ (deriv f) D) - (hf''_nonpos : ∀ x ∈ D, (deriv^[2] f x) ≤ 0) : concave_on D f := + (hf''_nonpos : ∀ x ∈ D, (deriv^[2] f x) ≤ 0) : concave_on ℝ D f := concave_on_of_deriv2_nonpos hD hf'.continuous_on (by simpa [hD₂.interior_eq] using hf') (by simpa [hD₂.interior_eq] using hf'') (by simpa [hD₂.interior_eq] using hf''_nonpos) @@ -1065,7 +1064,7 @@ concave_on_of_deriv2_nonpos hD hf'.continuous_on (by simpa [hD₂.interior_eq] u then `f` is convex on `ℝ`. -/ theorem convex_on_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : differentiable ℝ f) (hf'' : differentiable ℝ (deriv f)) (hf''_nonneg : ∀ x, 0 ≤ (deriv^[2] f x)) : - convex_on univ f := + convex_on ℝ univ f := convex_on_open_of_deriv2_nonneg convex_univ is_open_univ hf'.differentiable_on hf''.differentiable_on (λ x _, hf''_nonneg x) @@ -1073,7 +1072,7 @@ convex_on_open_of_deriv2_nonneg convex_univ is_open_univ hf'.differentiable_on then `f` is concave on `ℝ`. -/ theorem concave_on_univ_of_deriv2_nonpos {f : ℝ → ℝ} (hf' : differentiable ℝ f) (hf'' : differentiable ℝ (deriv f)) (hf''_nonpos : ∀ x, (deriv^[2] f x) ≤ 0) : - concave_on univ f := + concave_on ℝ univ f := concave_on_open_of_deriv2_nonpos convex_univ is_open_univ hf'.differentiable_on hf''.differentiable_on (λ x _, hf''_nonpos x) diff --git a/src/analysis/convex/exposed.lean b/src/analysis/convex/exposed.lean index d1271b51af267..41cb5c62180ca 100644 --- a/src/analysis/convex/exposed.lean +++ b/src/analysis/convex/exposed.lean @@ -164,12 +164,12 @@ begin exact hC.inter_left hCA, end -protected lemma is_extreme [normed_space ℝ E] (hAB : is_exposed ℝ A B) : - is_extreme ℝ A B := +protected lemma is_extreme (hAB : is_exposed 𝕜 A B) : + is_extreme 𝕜 A B := begin refine ⟨hAB.subset, λ x₁ x₂ hx₁A hx₂A x hxB hx, _⟩, obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩, - have hl : convex_on univ l := l.to_linear_map.convex_on convex_univ, + have hl : convex_on 𝕜 univ l := l.to_linear_map.convex_on convex_univ, have hlx₁ := hxB.2 x₁ hx₁A, have hlx₂ := hxB.2 x₂ hx₂A, refine ⟨⟨hx₁A, λ y hy, _⟩, ⟨hx₂A, λ y hy, _⟩⟩, @@ -179,8 +179,8 @@ begin exact hxB.2 y hy } end -protected lemma convex [normed_space ℝ E] (hAB : is_exposed ℝ A B) (hA : convex ℝ A) : - convex ℝ B := +protected lemma convex (hAB : is_exposed 𝕜 A B) (hA : convex 𝕜 A) : + convex 𝕜 B := begin obtain rfl | hB := B.eq_empty_or_nonempty, { exact convex_empty }, diff --git a/src/analysis/convex/extrema.lean b/src/analysis/convex/extrema.lean index 3287557a73a8c..a4da82694ffb6 100644 --- a/src/analysis/convex/extrema.lean +++ b/src/analysis/convex/extrema.lean @@ -26,7 +26,7 @@ open_locale classical Helper lemma for the more general case: `is_min_on.of_is_local_min_on_of_convex_on`. -/ lemma is_min_on.of_is_local_min_on_of_convex_on_Icc {f : ℝ → β} {a b : ℝ} (a_lt_b : a < b) - (h_local_min : is_local_min_on f (Icc a b) a) (h_conv : convex_on (Icc a b) f) : + (h_local_min : is_local_min_on f (Icc a b) a) (h_conv : convex_on ℝ (Icc a b) f) : ∀ x ∈ Icc a b, f a ≤ f x := begin by_contradiction H_cont, @@ -60,7 +60,7 @@ end A local minimum of a convex function is a global minimum, restricted to a set `s`. -/ lemma is_min_on.of_is_local_min_on_of_convex_on {f : E → β} {a : E} - (a_in_s : a ∈ s) (h_localmin : is_local_min_on f s a) (h_conv : convex_on s f) : + (a_in_s : a ∈ s) (h_localmin : is_local_min_on f s a) (h_conv : convex_on ℝ s f) : ∀ x ∈ s, f a ≤ f x := begin by_contradiction H_cont, @@ -91,18 +91,18 @@ end /-- A local maximum of a concave function is a global maximum, restricted to a set `s`. -/ lemma is_max_on.of_is_local_max_on_of_concave_on {f : E → β} {a : E} - (a_in_s : a ∈ s) (h_localmax: is_local_max_on f s a) (h_conc : concave_on s f) : + (a_in_s : a ∈ s) (h_localmax: is_local_max_on f s a) (h_conc : concave_on ℝ s f) : ∀ x ∈ s, f x ≤ f a := @is_min_on.of_is_local_min_on_of_convex_on _ (order_dual β) _ _ _ _ _ _ _ _ s f a a_in_s h_localmax h_conc /-- A local minimum of a convex function is a global minimum. -/ lemma is_min_on.of_is_local_min_of_convex_univ {f : E → β} {a : E} - (h_local_min : is_local_min f a) (h_conv : convex_on univ f) : ∀ x, f a ≤ f x := + (h_local_min : is_local_min f a) (h_conv : convex_on ℝ univ f) : ∀ x, f a ≤ f x := λ x, (is_min_on.of_is_local_min_on_of_convex_on (mem_univ a) (is_local_min.on h_local_min univ) h_conv) x (mem_univ x) /-- A local maximum of a concave function is a global maximum. -/ lemma is_max_on.of_is_local_max_of_convex_univ {f : E → β} {a : E} - (h_local_max : is_local_max f a) (h_conc : concave_on univ f) : ∀ x, f x ≤ f a := + (h_local_max : is_local_max f a) (h_conc : concave_on ℝ univ f) : ∀ x, f x ≤ f a := @is_min_on.of_is_local_min_of_convex_univ _ (order_dual β) _ _ _ _ _ _ _ _ f a h_local_max h_conc diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index fb521e6d13845..0ad50dcf9c3e9 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -13,13 +13,13 @@ inequality. The integral version can be found in `analysis.convex.integral`. A function `f : E → β` is `convex_on` a set `s` if `s` is itself a convex set, and for any two points `x y ∈ s`, the segment joining `(x, f x)` to `(y, f y)` is above the graph of `f`. -Equivalently, `convex_on 𝕜 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f z.1 ≤ p.2}` is +Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f z.1 ≤ p.2}` is a convex set. ## Main declarations -* `convex_on 𝕜 𝕜 s f`: The function `f` is convex on `s` with scalars `𝕜`. -* `concave_on 𝕜 𝕜 s f`: The function `f` is concave on `s` with scalars `𝕜`. +* `convex_on 𝕜 s f`: The function `f` is convex on `s` with scalars `𝕜`. +* `concave_on 𝕜 s f`: The function `f` is concave on `s` with scalars `𝕜`. * `convex_on.map_linear_combination_le` `convex_on.map_sum_le`: Convex Jensen's inequality. -/ @@ -479,8 +479,8 @@ begin end⟩ lemma concave_on_iff_div {f : E → β} : - concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b - → (a/(a+b)) • f x + (b/(a+b)) • f y ≤ f ((a/(a+b)) • x + (b/(a+b)) • y) := + concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b + → 0 < a + b → (a/(a+b)) • f x + (b/(a+b)) • f y ≤ f ((a/(a+b)) • x + (b/(a+b)) • y) := @convex_on_iff_div _ _ (order_dual β) _ _ _ _ _ _ _ /-- For a function `f` defined on a convex subset `D` of `𝕜`, if for any three points `x < y < z` diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index 0bee342349f07..ccd9551af1c35 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -108,7 +108,7 @@ to `s`, then the value of `g` at the average value of `f` is less than or equal of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_linear_combination_le` for a finite sum version of this lemma. -/ lemma convex_on.map_smul_integral_le [is_finite_measure μ] {s : set E} {g : E → ℝ} - (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} + (hg : convex_on ℝ s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) : g ((μ univ).to_real⁻¹ • ∫ x, f x ∂μ) ≤ (μ univ).to_real⁻¹ • ∫ x, g (f x) ∂μ := begin @@ -128,7 +128,7 @@ end of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_sum_le` for a finite sum version of this lemma. -/ lemma convex_on.map_integral_le [is_probability_measure μ] {s : set E} {g : E → ℝ} - (hg : convex_on s g) (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E} + (hg : convex_on ℝ s g) (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) : g (∫ x, f x ∂μ) ≤ ∫ x, g (f x) ∂μ := by simpa [measure_univ] diff --git a/src/analysis/convex/specific_functions.lean b/src/analysis/convex/specific_functions.lean index 93ff0be4c3c8e..3bca1de1375c8 100644 --- a/src/analysis/convex/specific_functions.lean +++ b/src/analysis/convex/specific_functions.lean @@ -16,7 +16,7 @@ In this file we prove that the following functions are convex: is convex on $(-∞, +∞)$; * `convex_on_pow` : for a natural $n$, the function $f(x)=x^n$ is convex on $[0, +∞)$; * `convex_on_fpow` : for an integer $m$, the function $f(x)=x^m$ is convex on $(0, +∞)$. -* `convex_on_rpow : ∀ p : ℝ, 1 ≤ p → convex_on (Ici 0) (λ x, x ^ p)` +* `convex_on_rpow : ∀ p : ℝ, 1 ≤ p → convex_on ℝ (Ici 0) (λ x, x ^ p)` * `concave_on_log_Ioi` and `concave_on_log_Iio`: log is concave on `Ioi 0` and `Iio 0` respectively. -/ @@ -24,12 +24,12 @@ open real set open_locale big_operators /-- `exp` is convex on the whole real line -/ -lemma convex_on_exp : convex_on univ exp := +lemma convex_on_exp : convex_on ℝ univ exp := convex_on_univ_of_deriv2_nonneg differentiable_exp (by simp) (assume x, (iter_deriv_exp 2).symm ▸ le_of_lt (exp_pos x)) /-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even -/ -lemma convex_on_pow_of_even {n : ℕ} (hn : even n) : convex_on set.univ (λ x : ℝ, x^n) := +lemma convex_on_pow_of_even {n : ℕ} (hn : even n) : convex_on ℝ set.univ (λ x : ℝ, x^n) := begin apply convex_on_univ_of_deriv2_nonneg differentiable_pow, { simp only [deriv_pow', differentiable.mul, differentiable_const, differentiable_pow] }, @@ -40,7 +40,7 @@ begin end /-- `x^n`, `n : ℕ` is convex on `[0, +∞)` for all `n` -/ -lemma convex_on_pow (n : ℕ) : convex_on (Ici 0) (λ x : ℝ, x^n) := +lemma convex_on_pow (n : ℕ) : convex_on ℝ (Ici 0) (λ x : ℝ, x^n) := begin apply convex_on_of_deriv2_nonneg (convex_Ici _) (continuous_pow n).continuous_on differentiable_on_pow, @@ -76,7 +76,7 @@ begin end /-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m` -/ -lemma convex_on_fpow (m : ℤ) : convex_on (Ioi 0) (λ x : ℝ, x^m) := +lemma convex_on_fpow (m : ℤ) : convex_on ℝ (Ioi 0) (λ x : ℝ, x^m) := begin have : ∀ n : ℤ, differentiable_on ℝ (λ x, x ^ n) (Ioi (0 : ℝ)), from λ n, differentiable_on_fpow _ _ (or.inl $ lt_irrefl _), @@ -91,7 +91,7 @@ begin exact int_prod_range_nonneg _ _ (nat.even_bit0 1) } end -lemma convex_on_rpow {p : ℝ} (hp : 1 ≤ p) : convex_on (Ici 0) (λ x : ℝ, x^p) := +lemma convex_on_rpow {p : ℝ} (hp : 1 ≤ p) : convex_on ℝ (Ici 0) (λ x : ℝ, x^p) := begin have A : deriv (λ (x : ℝ), x ^ p) = λ x, p * x^(p-1), by { ext x, simp [hp] }, apply convex_on_of_deriv2_nonneg (convex_Ici 0), @@ -108,7 +108,7 @@ begin exact mul_nonneg (sub_nonneg_of_le hp) (rpow_nonneg_of_nonneg (le_of_lt hx) _) } end -lemma concave_on_log_Ioi : concave_on (Ioi 0) log := +lemma concave_on_log_Ioi : concave_on ℝ (Ioi 0) log := begin have h₁ : Ioi 0 ⊆ ({0} : set ℝ)ᶜ, { intros x hx hx', @@ -126,7 +126,7 @@ begin exact neg_nonpos.mpr (inv_nonneg.mpr (sq_nonneg x)) } end -lemma concave_on_log_Iio : concave_on (Iio 0) log := +lemma concave_on_log_Iio : concave_on ℝ (Iio 0) log := begin have h₁ : Iio 0 ⊆ ({0} : set ℝ)ᶜ, { intros x hx hx', diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean index 6d5a0a8559cf1..504e686849074 100644 --- a/src/analysis/convex/topology.lean +++ b/src/analysis/convex/topology.lean @@ -181,7 +181,7 @@ section normed_space variables [normed_group E] [normed_space ℝ E] lemma convex_on_dist (z : E) (s : set E) (hs : convex ℝ s) : - convex_on s (λz', dist z' z) := + convex_on ℝ s (λz', dist z' z) := and.intro hs $ assume x y hx hy a b ha hb hab, calc From 452f3d89ea0b3e5ba08f5a61850b2ef641fffc72 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Thu, 23 Sep 2021 23:18:30 +0200 Subject: [PATCH 12/17] fix mean_inequalities --- docs/overview.yaml | 2 +- src/analysis/convex/integral.lean | 12 ++++++------ src/analysis/mean_inequalities.lean | 14 +++++++------- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index e3f3c0676c2f1..bcadbe8ba9817 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -272,7 +272,7 @@ Analysis: Convexity: convex function: 'convex_on' characterization of convexity: 'convex_on_of_deriv2_nonneg' - Jensen's inequality (finite sum version): 'convex_on.map_sum_le' + Jensen's inequality (finite sum version): 'convex_on.map_linear_combination_le' Jensen's inequality (integral version): 'convex_on.map_integral_le' convexity inequalities: 'analysis/mean_inequalities.html' Carathéodory's theorem: 'convex_hull_eq_union' diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index ccd9551af1c35..f75d8e751ac72 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -32,7 +32,7 @@ In this file we prove four theorems: continuous on a convex closed set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected value of `g ∘ f` provided that both `f` and `g ∘ f` are - integrable. See also `convex.map_sum_le` for a finite sum version of this lemma. + integrable. See also `convex_on.map_linear_combination_le` for a finite sum version of this lemma. ## Tags @@ -122,11 +122,11 @@ begin using (ht_conv.smul_integral_mem ht_closed hμ ht_mem (hfi.prod_mk hgi)).2 end -/-- Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set -`s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to -`s`, then the value of `g` at the expected value of `f` is less than or equal to the expected value -of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_sum_le` for a -finite sum version of this lemma. -/ +/-- Convex **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex +closed set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. +points to `s`, then the value of `g` at the expected value of `f` is less than or equal to the +expected value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also +`convex_on.map_linear_combination_le` for a finite sum version of this lemma. -/ lemma convex_on.map_integral_le [is_probability_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on ℝ s g) (hgc : continuous_on g s) (hsc : is_closed s) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) : diff --git a/src/analysis/mean_inequalities.lean b/src/analysis/mean_inequalities.lean index 6a721629e4ca7..0ac50272fc803 100644 --- a/src/analysis/mean_inequalities.lean +++ b/src/analysis/mean_inequalities.lean @@ -15,7 +15,7 @@ these inequalities are available in `measure_theory.mean_inequalities`. ## Main theorems -### AM-GM inequality: +### AM-GM inequality The inequality says that the geometric mean of a tuple of non-negative numbers is less than or equal to their arithmetic mean. We prove the weighted version of this inequality: if $w$ and $z$ @@ -127,8 +127,8 @@ begin -- If all numbers `z i` with non-zero weight are positive, then we apply Jensen's inequality -- for `exp` and numbers `log (z i)` with weights `w i`. { simp only [not_exists, not_and, ne.def, not_not] at A, - have := convex_on_exp.map_sum_le hw hw' (λ i _, set.mem_univ $ log (z i)), - simp only [exp_sum, (∘), smul_eq_mul, mul_comm (w _) (log _)] at this, + have := convex_on_exp.map_linear_combination_le hw hw' (λ i _, set.mem_univ $ log (z i)), + simp only [linear_combination, exp_sum, (∘), smul_eq_mul, mul_comm (w _) (log _)] at this, convert this using 1; [apply prod_congr rfl, apply sum_congr rfl]; intros i hi, { cases eq_or_lt_of_le (hz i hi) with hz hz, { simp [A i hi hz.symm] }, @@ -141,22 +141,22 @@ end theorem pow_arith_mean_le_arith_mean_pow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (n : ℕ) : (∑ i in s, w i * z i) ^ n ≤ ∑ i in s, (w i * z i ^ n) := -(convex_on_pow n).map_sum_le hw hw' hz +(convex_on_pow n).map_linear_combination_le hw hw' hz theorem pow_arith_mean_le_arith_mean_pow_of_even (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i in s, w i = 1) {n : ℕ} (hn : even n) : (∑ i in s, w i * z i) ^ n ≤ ∑ i in s, (w i * z i ^ n) := -(convex_on_pow_of_even hn).map_sum_le hw hw' (λ _ _, trivial) +(convex_on_pow_of_even hn).map_linear_combination_le hw hw' (λ _ _, trivial) theorem fpow_arith_mean_le_arith_mean_fpow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 < z i) (m : ℤ) : (∑ i in s, w i * z i) ^ m ≤ ∑ i in s, (w i * z i ^ m) := -(convex_on_fpow m).map_sum_le hw hw' hz +(convex_on_fpow m).map_linear_combination_le hw hw' hz theorem rpow_arith_mean_le_arith_mean_rpow (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) {p : ℝ} (hp : 1 ≤ p) : (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, (w i * z i ^ p) := -(convex_on_rpow hp).map_sum_le hw hw' hz +(convex_on_rpow hp).map_linear_combination_le hw hw' hz theorem arith_mean_le_rpow_mean (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) {p : ℝ} (hp : 1 ≤ p) : From 113551619c52013017960984d43b324a4f4da74c Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Fri, 24 Sep 2021 22:32:22 +0200 Subject: [PATCH 13/17] revert some more --- docs/overview.yaml | 2 +- src/analysis/convex/basic.lean | 4 ++-- src/analysis/convex/function.lean | 2 +- src/analysis/convex/integral.lean | 23 +++++++++++------------ 4 files changed, 15 insertions(+), 16 deletions(-) diff --git a/docs/overview.yaml b/docs/overview.yaml index 516101bd4fac9..e3f3c0676c2f1 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -272,7 +272,7 @@ Analysis: Convexity: convex function: 'convex_on' characterization of convexity: 'convex_on_of_deriv2_nonneg' - Jensen's inequality (finite sum version): 'convex_on.map_center_mass_le' + Jensen's inequality (finite sum version): 'convex_on.map_sum_le' Jensen's inequality (integral version): 'convex_on.map_integral_le' convexity inequalities: 'analysis/mean_inequalities.html' Carathéodory's theorem: 'convex_hull_eq_union' diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean index ec32d6f6fbcc8..7438232083a1e 100644 --- a/src/analysis/convex/basic.lean +++ b/src/analysis/convex/basic.lean @@ -404,7 +404,7 @@ section add_comm_monoid variables [add_comm_monoid E] /-- Convexity of sets. -/ -def convex [has_scalar 𝕜 E](s : set E) := +def convex [has_scalar 𝕜 E] (s : set E) := ∀ ⦃x y : E⦄, x ∈ s → y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s @@ -1035,7 +1035,7 @@ end convex_hull section simplex -variables (ι : Type*) [ordered_semiring 𝕜] [add_comm_group E] [fintype ι] [module 𝕜 E] +variables (ι : Type*) [ordered_semiring 𝕜] [fintype ι] /-- The standard simplex in the space of functions `ι → 𝕜` is the set of vectors with non-negative coordinates with total sum `1`. This is the free object in the category of convex spaces.-/ diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index 81cbf0d8bc61c..7a39912be1a38 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -15,7 +15,7 @@ inequality. The integral version can be found in `analysis.convex.integral`. A function `f : E → β` is `convex_on` a set `s` if `s` is itself a convex set, and for any two points `x y ∈ s`, the segment joining `(x, f x)` to `(y, f y)` is above the graph of `f`. -Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f z.1 ≤ p.2}` is +Equivalently, `convex_on 𝕜 f s` means that the epigraph `{p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}` is a convex set. ## Main declarations diff --git a/src/analysis/convex/integral.lean b/src/analysis/convex/integral.lean index 35556debff1ca..cabfade17b69c 100644 --- a/src/analysis/convex/integral.lean +++ b/src/analysis/convex/integral.lean @@ -18,21 +18,20 @@ In this file we prove four theorems: * `convex.integral_mem`: if `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` - belongs to `s`: `∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` for a finite sum - version of this lemma. + belongs to `s`: `∫ x, f x ∂μ ∈ s`. See also `convex.sum_mem` for a finite sum version of this + lemma. * `convex_on.map_smul_integral_le`: Convex Jensen's inequality: If a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to the average value of `g ∘ f` provided that both `f` and - `g ∘ f` are integrable. See also `convex_on.map_center_mass_le` for a finite sum version of - this lemma. + `g ∘ f` are integrable. See also `convex_on.map_sum_le` for a finite sum version of this lemma. * `convex_on.map_integral_le`: Convex Jensen's inequality: If a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected value of `g ∘ f` provided that both `f` and `g ∘ f` are - integrable. See also `convex_on.map_center_mass_le` for a finite sum version of this lemma. + integrable. See also `convex_on.map_sum_le` for a finite sum version of this lemma. ## Tags @@ -67,9 +66,9 @@ begin by rw [← (F n).sum_range_measure_preimage_singleton, @ennreal.to_real_sum _ _ (λ y, μ ((F n) ⁻¹' {y})) (λ _ _, (measure_ne_top _ _))], rw [← this, simple_func.integral], - refine hs.center_mass_mem' (λ _ _, ennreal.to_real_nonneg) _ _, - { rw [this, ne.def, ennreal.to_real_eq_zero_iff, measure.measure_univ_eq_zero], - exact not_or hμ (measure_ne_top _ _) }, + refine hs.center_mass_mem (λ _ _, ennreal.to_real_nonneg) _ _, + { rw [this, ennreal.to_real_pos_iff, pos_iff_ne_zero, ne.def, measure.measure_univ_eq_zero], + exact ⟨hμ, measure_ne_top _ _⟩ }, { simp only [simple_func.mem_range], rintros _ ⟨x, rfl⟩, exact simple_func.approx_on_mem hfm h₀ n x } @@ -77,8 +76,8 @@ end /-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`: -`(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` for a finite sum -version of this lemma. -/ +`(μ univ).to_real⁻¹ • ∫ x, f x ∂μ ∈ s`. See also `convex.center_mass_mem` for a finite sum version +of this lemma. -/ lemma convex.smul_integral_mem [is_finite_measure μ] {s : set E} (hs : convex ℝ s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) : @@ -105,8 +104,8 @@ by simpa [measure_univ] using hs.smul_integral_mem hsc (is_probability_measure.n /-- Jensen's inequality: if a function `g : E → ℝ` is convex and continuous on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to the average value -of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also -`convex.map_center_mass_le` for a finite sum version of this lemma. -/ +of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also `convex.map_center_mass_le` +for a finite sum version of this lemma. -/ lemma convex_on.map_smul_integral_le [is_finite_measure μ] {s : set E} {g : E → ℝ} (hg : convex_on ℝ s g) (hgc : continuous_on g s) (hsc : is_closed s) (hμ : μ ≠ 0) {f : α → E} (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : integrable f μ) (hgi : integrable (g ∘ f) μ) : From 6d179d2cd77158cb72db0d3a853126d3898e2b7a Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Sat, 25 Sep 2021 08:53:26 +0200 Subject: [PATCH 14/17] fix combination --- src/analysis/convex/combination.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 03c49245371b2..041d1e23be513 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -278,7 +278,7 @@ The map is defined in terms of operations on `(s → ℝ) →ₗ[ℝ] ℝ` so th to prove that this map is linear. -/ lemma set.finite.convex_hull_eq_image {s : set E} (hs : finite 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) := + (⇑(∑ x : s, (@linear_map.proj R s _ (λ i, R) _ _ x).smul_right x.1)) '' (std_simplex R s) := begin rw [← convex_hull_basis_eq_std_simplex, ← linear_map.convex_hull_image, ← set.range_comp, (∘)], apply congr_arg, From ed6fc38ac08dcc2bd7dc46109571670b4930128b Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Sat, 25 Sep 2021 14:20:45 +0200 Subject: [PATCH 15/17] fix Jensen and maximum principle --- src/analysis/convex/combination.lean | 2 +- src/analysis/convex/exposed.lean | 2 +- src/analysis/convex/function.lean | 78 +++++++++++++++------------- 3 files changed, 45 insertions(+), 37 deletions(-) diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 041d1e23be513..63cf784c230e5 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -27,7 +27,7 @@ open_locale big_operators classical universes u u' variables {R E F ι ι' : Type*} - [linear_ordered_field R] [add_comm_group E] [module R E] [add_comm_group F] [module R F] + [linear_ordered_field R] [add_comm_monoid 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. diff --git a/src/analysis/convex/exposed.lean b/src/analysis/convex/exposed.lean index 41cb5c62180ca..f12467c6cb686 100644 --- a/src/analysis/convex/exposed.lean +++ b/src/analysis/convex/exposed.lean @@ -186,7 +186,7 @@ begin { exact convex_empty }, obtain ⟨l, rfl⟩ := hAB hB, exact λ x₁ x₂ hx₁ hx₂ a b ha hb hab, ⟨hA hx₁.1 hx₂.1 ha hb hab, λ y hy, - ((l.to_linear_map.concave_on convex_univ).concave_le _ + ((l.to_linear_map.concave_on convex_univ).concave_ge _ ⟨mem_univ _, hx₁.2 y hy⟩ ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩, end diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index 7a39912be1a38..527fe569a1d90 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -108,7 +108,7 @@ lemma convex_on.convex_le (hf : convex_on 𝕜 s f) (r : β) : (smul_le_smul_of_nonneg hy.2 hb) ... = r : convex.combo_self hab r⟩ -lemma concave_on.concave_le (hf : concave_on 𝕜 s f) (r : β) : +lemma concave_on.concave_ge (hf : concave_on 𝕜 s f) (r : β) : convex 𝕜 {x ∈ s | r ≤ f x} := @convex_on.convex_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ f hf r @@ -607,8 +607,8 @@ variables [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_mono /-- Convex **Jensen's inequality**, `finset.center_mass` version. -/ lemma convex_on.map_center_mass_le (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) - (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : - f (t.center_mass p w) ≤ t.center_mass (f ∘ p) w := + (h₁ : 0 < ∑ i in t, w i) (hmem : ∀ i ∈ t, p i ∈ s) : + f (t.center_mass w p) ≤ t.center_mass w (f ∘ p) := begin have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}, from λ i hi, ⟨hmem i hi, le_rfl⟩, @@ -619,25 +619,21 @@ end /-- Concave **Jensen's inequality**, `finset.center_mass` version. -/ lemma concave_on.le_map_center_mass (hf : concave_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) - (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : - t.center_mass (f ∘ p) w ≤ f (t.center_mass p w) := + (h₁ : 0 < ∑ i in t, w i) (hmem : ∀ i ∈ t, p i ∈ s) : + t.center_mass w (f ∘ p) ≤ f (t.center_mass w p) := @convex_on.map_center_mass_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ _ _ _ _ hf h₀ h₁ hmem /-- Convex **Jensen's inequality**, `finset.sum` version. -/ -lemma convex_on.map_sum_le (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i ≠ 0) +lemma convex_on.map_sum_le (hf : convex_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : - f ((∑ i in t, w i)⁻¹ • ∑ i in t, w i • p i) ≤ (∑ i in t, w i)⁻¹ • ∑ i in t, w i • f (p i) := -begin - rw [←center_mass, ←center_mass_smul_right, ←center_mass, - ←center_mass_smul_right], - exact hf.map_center_mass_le (center_mass_normalize_weight_nonneg h₀) - (center_mass_normalize_weight_sum h₁) hmem, -end + f (∑ i in t, w i • p i) ≤ ∑ i in t, w i • f (p i) := +by simpa only [center_mass, h₁, inv_one, one_smul] + using hf.map_center_mass_le h₀ (h₁.symm ▸ zero_lt_one) hmem /-- Concave **Jensen's inequality**, `finset.sum` version. -/ -lemma concave_on.le_map_sum (hf : concave_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i ≠ 0) +lemma concave_on.le_map_sum (hf : concave_on 𝕜 s f) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) : - (∑ i in t, w i)⁻¹ • ∑ i in t, w i • f (p i) ≤ f ((∑ i in t, w i)⁻¹ • ∑ i in t, w i • p i) := + ∑ i in t, w i • f (p i) ≤ f (∑ i in t, w i • p i) := @convex_on.map_sum_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ _ _ _ _ hf h₀ h₁ hmem end jensen @@ -645,40 +641,52 @@ end jensen /-! ### Maximum principle -/ section maximum_principle -variables [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] - [mul_action_with_zero 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {t : finset ι} {w : ι → 𝕜} +variables [linear_ordered_field 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_group β] + [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {t : finset ι} {w : ι → 𝕜} {p : ι → E} -/-- If a function `f` is convex on `s` takes value `y` at the center of mass of some points -`p i ∈ s`, then for some `i` we have `y ≤ f (p i)`. -/ -lemma convex_on.exists_ge_of_center_mass {f : E → 𝕜} (h : convex_on 𝕜 s f) - (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, p i ∈ s) : - ∃ i ∈ t, f (t.center_mass p w) ≤ f (p i) := +/-- If a function `f` is convex on `s`, then the value it takes at some center of mass of points of +`s` is less than the value it takes on one of those points. -/ +lemma convex_on.exists_ge_of_center_mass (h : convex_on 𝕜 s f) + (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i in t, w i) (hp : ∀ i ∈ t, p i ∈ s) : + ∃ i ∈ t, f (t.center_mass w p) ≤ f (p i) := begin - set y := t.center_mass p w, + set y := t.center_mass w p, suffices h : ∃ i ∈ t.filter (λ i, w i ≠ 0), w i • f y ≤ w i • (f ∘ p) i, { obtain ⟨i, hi, hfi⟩ := h, rw mem_filter at hi, exact ⟨i, hi.1, (smul_le_smul_iff_of_pos $ (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩ }, - refine exists_le_of_sum_le _ _, - { have := @zero_ne_one 𝕜 _ _, - rw [←hw₁, ←sum_filter_ne_zero] at this, - exact nonempty_of_sum_ne_zero this.symm }, - { rw [←center_mass, ←center_mass, finset.center_mass_filter_ne_zero, - finset.center_mass_filter_ne_zero, center_mass_const_left, hw₁, one_smul], - exact h.map_center_mass_le hw₀ hw₁ hz } + have hw' : (0 : 𝕜) < ∑ i in filter (λ i, w i ≠ 0) t, w i := by rwa sum_filter_ne_zero, + refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') _, + rw [←sum_smul, ←smul_le_smul_iff_of_pos (inv_pos.2 hw'), inv_smul_smul' hw'.ne', + ←finset.center_mass, finset.center_mass_filter_ne_zero], + exact h.map_center_mass_le hw₀ hw₁ hp, + apply_instance, end +/-- If a function `f` is concave on `s`, then the value it takes at some center of mass of points of +`s` is greater than the value it takes on one of those points. -/ +lemma concave_on.exists_le_of_center_mass (h : concave_on 𝕜 s f) + (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i in t, w i) (hp : ∀ i ∈ t, p i ∈ s) : + ∃ i ∈ t, f (p i) ≤ f (t.center_mass w p) := +@convex_on.exists_ge_of_center_mass 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ _ _ _ _ h hw₀ hw₁ hp + /-- Maximum principle for convex functions. If a function `f` is convex on the convex hull of `s`, -then `f` reaches a maximum on `convex_hull 𝕜 s` outside of `s`. -/ -lemma convex_on.exists_ge_of_mem_convex_hull {f : E → 𝕜} (hf : convex_on 𝕜 (convex_hull 𝕜 s) f) - {x} (hx : x ∈ convex_hull 𝕜 s) : ∃ y ∈ s, f x ≤ f y := +then the eventual maximum of `f` on `convex_hull 𝕜 s` lies in `s`. -/ +lemma convex_on.exists_ge_of_mem_convex_hull (hf : convex_on 𝕜 (convex_hull 𝕜 s) f) {x} + (hx : x ∈ convex_hull 𝕜 s) : ∃ y ∈ s, f x ≤ f y := begin - rw convex_hull_eq at hx, + rw _root_.convex_hull_eq at hx, obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx, - rcases hf.exists_ge_of_center_mass hw₀ hw₁ + rcases hf.exists_ge_of_center_mass hw₀ (hw₁.symm ▸ zero_lt_one) (λ i hi, subset_convex_hull 𝕜 s (hp i hi)) with ⟨i, hit, Hi⟩, exact ⟨p i, hp i hit, Hi⟩ end +/-- Minimum principle for concave functions. If a function `f` is concave on the convex hull of `s`, +then the eventual minimum of `f` on `convex_hull 𝕜 s` lies in `s`. -/ +lemma concave_on.exists_le_of_mem_convex_hull (hf : concave_on 𝕜 (convex_hull 𝕜 s) f) {x} + (hx : x ∈ convex_hull 𝕜 s) : ∃ y ∈ s, f y ≤ f x := +@convex_on.exists_ge_of_mem_convex_hull 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ hf _ hx + end maximum_principle From d84a2d1dff5fa3cf7cce014b64920adb17d306f2 Mon Sep 17 00:00:00 2001 From: YaelDillies Date: Sun, 26 Sep 2021 10:54:12 +0200 Subject: [PATCH 16/17] revert std_simplex --- src/analysis/convex/basic.lean | 17 ++++++++++------- src/analysis/convex/combination.lean | 15 +++++++-------- src/analysis/convex/topology.lean | 18 +++++++++--------- 3 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean index 7438232083a1e..caf06ae70bb4d 100644 --- a/src/analysis/convex/basic.lean +++ b/src/analysis/convex/basic.lean @@ -1035,18 +1035,21 @@ end convex_hull section simplex -variables (ι : Type*) [ordered_semiring 𝕜] [fintype ι] +variables (ι : Type*) [fintype ι] -/-- The standard simplex in the space of functions `ι → 𝕜` is the set of vectors with non-negative -coordinates with total sum `1`. This is the free object in the category of convex spaces.-/ -def std_simplex : set (ι → 𝕜) := +/-- 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 ι] (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] }, @@ -1057,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 diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean index 63cf784c230e5..8fa307c5dd118 100644 --- a/src/analysis/convex/combination.lean +++ b/src/analysis/convex/combination.lean @@ -26,9 +26,7 @@ open set open_locale big_operators classical universes u u' -variables {R E F ι ι' : Type*} - [linear_ordered_field R] [add_comm_monoid E] [module R E] [add_comm_group F] [module R F] - {s : set E} +variables {R E ι ι' : Type*} [linear_ordered_field R] [add_comm_monoid E] [module R E] {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`. -/ @@ -256,11 +254,11 @@ end variables (ι) [fintype ι] {f : ι → R} -/-- `std_simplex R ι` is the convex hull of the canonical basis in `ι → R`. -/ +/-- `std_simplex ι` is the convex hull of the canonical basis in `ι → ℝ`. -/ lemma convex_hull_basis_eq_std_simplex : - convex_hull R (range $ λ(i j:ι), if i = j then (1:R) else 0) = std_simplex R ι := + 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 R ι)) _, + refine subset.antisymm (convex_hull_min _ (convex_std_simplex ι R)) _, { rintros _ ⟨i, rfl⟩, exact ite_eq_mem_std_simplex R i }, { rintros w ⟨hw₀, hw₁⟩, @@ -273,12 +271,13 @@ variable {ι} /-- The convex hull of a finite set is the image of the standard simplex in `s → ℝ` under the linear map sending each function `w` to `∑ x in s, w x • x`. + Since we have no sums over finite sets, we use sum over `@finset.univ _ hs.fintype`. 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 R s = by haveI := hs.fintype; exact - (⇑(∑ x : s, (@linear_map.proj R s _ (λ i, R) _ _ x).smul_right x.1)) '' (std_simplex R s) := + (⇑(∑ 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, @@ -288,6 +287,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 R ι) (x) : +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)⟩ diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean index 504e686849074..54adcb753725a 100644 --- a/src/analysis/convex/topology.lean +++ b/src/analysis/convex/topology.lean @@ -42,9 +42,9 @@ section std_simplex variables [fintype ι] -/-- Every vector in `std_simplex ℝ ι` has `max`-norm at most `1`. -/ +/-- 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], @@ -56,18 +56,18 @@ end variable (ι) -/-- `std_simplex ℝ ι` is bounded. -/ -lemma bounded_std_simplex : metric.bounded (std_simplex ℝ ι) := +/-- `std_simplex ι` is bounded. -/ +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 +/-- `std_simplex ι` is closed. -/ +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 ℝ ι) := +/-- `std_simplex ι` is compact. -/ +lemma compact_std_simplex : is_compact (std_simplex ι ℝ) := metric.compact_iff_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩ end std_simplex From 801d4944303f89a0319fd2382f124e0cdf0ddce5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 27 Sep 2021 07:49:57 +0200 Subject: [PATCH 17/17] indentation Co-authored-by: Scott Morrison --- src/analysis/convex/function.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/convex/function.lean b/src/analysis/convex/function.lean index 527fe569a1d90..05fc99b565063 100644 --- a/src/analysis/convex/function.lean +++ b/src/analysis/convex/function.lean @@ -62,7 +62,7 @@ lemma convex_on.subset {f : E → β} {t : set E} (hf : convex_on 𝕜 t f) (hst ⟨hs, λ x y hx hy, hf.2 (hst hx) (hst hy)⟩ lemma concave_on.subset {f : E → β} {t : set E} (hf : concave_on 𝕜 t f) (hst : s ⊆ t) -(hs : convex 𝕜 s) : concave_on 𝕜 s f := + (hs : convex 𝕜 s) : concave_on 𝕜 s f := ⟨hs, λ x y hx hy, hf.2 (hst hx) (hst hy)⟩ end has_scalar