feat(analysis/convex/jensen): Maximum modulus principle for finsets (#17091)

YaelDillies · YaelDillies · commit bfad3f455b38 · 2022-11-09T08:04:03.000Z
A convex function on the convex hull of a finset is bounded by its supremum on the finset.
diff --git a/src/analysis/convex/combination.lean b/src/analysis/convex/combination.lean
@@ -27,8 +27,9 @@ open set function
 open_locale big_operators classical pointwise
 
 universes u u'
-variables {R E F ι ι' : Type*} [linear_ordered_field R] [add_comm_group E] [add_comm_group F]
-  [module R E] [module R F] {s : set E}
+variables {R E F ι ι' α : Type*} [linear_ordered_field R] [add_comm_group E] [add_comm_group F]
+  [linear_ordered_add_comm_group α] [module R E] [module R F] [module R α] [ordered_smul R α]
+  {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`. -/
@@ -119,6 +120,25 @@ lemma finset.center_mass_filter_ne_zero :
 finset.center_mass_subset z (filter_subset _ _) $ λ i hit hit',
   by simpa only [hit, mem_filter, true_and, ne.def, not_not] using hit'
 
+namespace finset
+
+lemma center_mass_le_sup {s : finset ι} {f : ι → α} {w : ι → R}
+  (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i in s, w i) :
+  s.center_mass w f ≤ s.sup' (nonempty_of_ne_empty $ by { rintro rfl, simpa using hw₁ }) f :=
+begin
+  rw [center_mass, inv_smul_le_iff hw₁, sum_smul],
+  exact sum_le_sum (λ i hi, smul_le_smul_of_nonneg (le_sup' _ hi) $ hw₀ i hi),
+  apply_instance,
+end
+
+lemma inf_le_center_mass {s : finset ι} {f : ι → α} {w : ι → R}
+  (hw₀ : ∀ i ∈ s, 0 ≤ w i) (hw₁ : 0 < ∑ i in s, w i) :
+  s.inf' (nonempty_of_ne_empty $ by { rintro rfl, simpa using hw₁ }) f ≤ s.center_mass w f :=
+@center_mass_le_sup R _ αᵒᵈ _ _ _ _ _ _ _ hw₀ hw₁
+
+end finset
+
+
 variable {z}
 
 /-- The center of mass of a finite subset of a convex set belongs to the set
@@ -318,6 +338,11 @@ begin
       (hw₁.symm ▸ zero_lt_one) (λ x hx, hx) }
 end
 
+lemma finset.mem_convex_hull {s : finset E} {x : E} :
+  x ∈ convex_hull R (s : set E) ↔
+    ∃ (w : E → R) (hw₀ : ∀ y ∈ s, 0 ≤ w y) (hw₁ : ∑ y in s, w y = 1), s.center_mass w id = x :=
+by rw [finset.convex_hull_eq, set.mem_set_of_eq]
+
 lemma set.finite.convex_hull_eq {s : set E} (hs : s.finite) :
   convex_hull R s = {x : E | ∃ (w : E → R) (hw₀ : ∀ y ∈ s, 0 ≤ w y)
     (hw₁ : ∑ y in hs.to_finset, w y = 1), hs.to_finset.center_mass w id = x} :=
diff --git a/src/analysis/convex/jensen.lean b/src/analysis/convex/jensen.lean
@@ -74,7 +74,21 @@ end jensen
 section maximum_principle
 variables [linear_ordered_field 𝕜] [add_comm_group E] [linear_ordered_add_comm_group β]
   [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {t : finset ι} {w : ι → 𝕜}
-  {p : ι → E}
+  {p : ι → E} {x : E}
+
+lemma le_sup_of_mem_convex_hull {s : finset E} (hf : convex_on 𝕜 (convex_hull 𝕜 (s : set E)) f)
+  (hx : x ∈ convex_hull 𝕜 (s : set E)) :
+  f x ≤ s.sup' (coe_nonempty.1 $ convex_hull_nonempty_iff.1 ⟨x, hx⟩) f :=
+begin
+  obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convex_hull.1 hx,
+  exact (hf.map_center_mass_le hw₀ (by positivity) $ subset_convex_hull _ _).trans
+    (center_mass_le_sup hw₀ $ by positivity),
+end
+
+lemma inf_le_of_mem_convex_hull {s : finset E} (hf : concave_on 𝕜 (convex_hull 𝕜 (s : set E)) f)
+  (hx : x ∈ convex_hull 𝕜 (s : set E)) :
+  s.inf' (coe_nonempty.1 $ convex_hull_nonempty_iff.1 ⟨x, hx⟩) f ≤ f x :=
+le_sup_of_mem_convex_hull hf.dual hx
 
 /-- 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. -/
