Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - split(analysis/convex/combination): split off analysis.convex.basic #9115

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - split(analysis/convex/combination): split off analysis.convex.basic #9115

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
30ae83b
initial commit
YaelDillies Sep 9, 2021
4536b54
fix
YaelDillies Sep 9, 2021
d44b25a
fix topology
YaelDillies Sep 10, 2021
4aaf981
Merge remote-tracking branch 'origin/master' into yael/center_mass
YaelDillies Sep 10, 2021
fecaf48
mention of Jensen
YaelDillies Sep 11, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
291 changes: 0 additions & 291 deletions src/analysis/convex/basic.lean
View file
Open in desktop
Expand Up @@ -1176,192 +1176,6 @@ by simpa only [add_comm] using hf.translate_right

end functions

/-! ### Center of mass -/

section center_mass

/-- 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)

variables (i j : ι) (c : ℝ) (t : finset ι) (w : ι → ℝ) (z : ι → E)

open finset

lemma finset.center_mass_empty : (∅ : finset ι).center_mass w z = 0 :=
by simp only [center_mass, sum_empty, smul_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 :=
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 :=
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 :=
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 :=
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 :=
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
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) :=
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] }
end

/-- A convex combination of two centers of mass is a center of mass as well. This version
works if two centers of mass share the set of original points. -/
lemma finset.center_mass_segment
(s : finset ι) (w₁ w₂ : ι → ℝ) (z : ι → E)
(hw₁ : ∑ i in s, w₁ i = 1) (hw₂ : ∑ i in s, w₂ i = 1) (a b : ℝ) (hab : a + b = 1) :
a • s.center_mass w₁ z + b • s.center_mass w₂ z =
s.center_mass (λ i, a * w₁ i + b * w₂ i) z :=
have hw : ∑ i in s, (a * w₁ i + b * w₂ i) = 1,
by simp only [mul_sum.symm, sum_add_distrib, mul_one, *],
by simp only [finset.center_mass_eq_of_sum_1, smul_sum, sum_add_distrib, add_smul, mul_smul, *]

lemma finset.center_mass_ite_eq (hi : i ∈ t) :
t.center_mass (λ j, if (i = j) then 1 else 0) z = z i :=
begin
rw [finset.center_mass_eq_of_sum_1],
transitivity ∑ j in t, if (i = j) then z 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}

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 :=
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]
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',
by simpa only [hit, mem_filter, true_and, ne.def, not_not] using hit'

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 :=
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 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]),
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],
exact zi },
{ rw [finset.center_mass_insert _ _ _ hi hsum_t],
refine convex_iff_div.1 hs zi (ht hs₀ _ _) _ (sum_nonneg hs₀) hpos,
{ 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)
(hz : ∀ i ∈ t, z i ∈ s) :
∑ i in t, w i • z i ∈ s :=
by simpa only [h₁, center_mass, inv_one, one_smul] using
hs.center_mass_mem h₀ (h₁.symm ▸ zero_lt_one) hz

lemma convex_iff_sum_mem :
convex s ↔
(∀ (t : finset E) (w : E → ℝ),
(∀ 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, _⟩,
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) _ _ _,
{ 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] },
{ simp only [sum_pair h_cases, if_neg h_cases, if_pos rfl, hab] },
{ simp_intros i hi,
cases hi; subst i; simp [hx, hy, if_neg h_cases] } }
end

/-- 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) :=
begin
have hmem' : ∀ i ∈ t, (z i, (f ∘ z) i) ∈ {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2},
from λ i hi, ⟨hmem i hi, le_refl _⟩,
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]
end

/-- 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

/-- 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) :=
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
end

end center_mass

/-! ### Convex hull -/

section convex_hull
Expand Down Expand Up @@ -1459,98 +1273,6 @@ lemma is_linear_map.image_convex_hull {f : E → F} (hf : is_linear_map ℝ f) :
f '' (convex_hull s) = convex_hull (f '' s) :=
(hf.mk' f).image_convex_hull

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)

-- TODO : Do we need other versions of the next lemma?

/-- Convex hull of `s` is equal to the set of all centers of masses of `finset`s `t`, `z '' t ⊆ s`.
This version allows finsets in any type in any universe. -/
lemma convex_hull_eq (s : set E) :
convex_hull s = {x : E | ∃ (ι : Type u') (t : finset ι) (w : ι → ℝ) (z : ι → E)
(hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i in t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s),
t.center_mass w z = x} :=
begin
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] },
{ 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],
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₀] },
{ 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 t.center_mass_mem_convex_hull hw₀ (hw₁.symm ▸ zero_lt_one) 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`. -/
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,
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⟩
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} :=
begin
refine subset.antisymm (convex_hull_min _ _) _,
{ intros x hx,
rw [finset.mem_coe] at hx,
refine ⟨_, _, _, finset.center_mass_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],
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)
(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} :=
by simpa only [set.finite.coe_to_finset, set.finite.mem_to_finset, exists_prop]
using hs.to_finset.convex_hull_eq

lemma 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 _ _,
{ rw [convex_hull_eq.{u}],
rintros x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩,
simp only [mem_Union],
refine ⟨t.image z, _, _⟩,
{ rw [finset.coe_image, image_subset_iff],
exact hz },
{ 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) } } },
{ exact Union_subset (λ i, Union_subset convex_hull_mono), },
end

lemma is_linear_map.convex_hull_image {f : E → F} (hf : is_linear_map ℝ f) (s : set E) :
convex_hull (f '' s) = f '' convex_hull s :=
set.subset.antisymm (convex_hull_min (image_subset _ (subset_convex_hull s)) $
Expand Down Expand Up @@ -1594,19 +1316,6 @@ variable {ι}
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 _)]⟩

/-- `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 ι :=
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)
(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 → ℝ`
Expand Down
2 changes: 1 addition & 1 deletion src/analysis/convex/caratheodory.lean
View file
Open in desktop
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Scott Morrison
-/
import analysis.convex.basic
import analysis.convex.combination
import linear_algebra.affine_space.independent

/-!
Expand Down