Skip to content

Commit ba1c53b

Browse files
FordUniverFordUniver
committed
merge: include feat/convex-first-order-inequalities (#26) for Baillon-Haddad's ConvexOn.add_inner_gradient_le
2 parents 9f05f69 + f96e7eb commit ba1c53b

5 files changed

Lines changed: 534 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1909,17 +1909,20 @@ public import Mathlib.Analysis.Convex.EGauge
19091909
public import Mathlib.Analysis.Convex.Exposed
19101910
public import Mathlib.Analysis.Convex.Extrema
19111911
public import Mathlib.Analysis.Convex.Extreme
1912+
public import Mathlib.Analysis.Convex.FDeriv
19121913
public import Mathlib.Analysis.Convex.Function
19131914
public import Mathlib.Analysis.Convex.FunctionTopology
19141915
public import Mathlib.Analysis.Convex.Gauge
19151916
public import Mathlib.Analysis.Convex.GaugeRescale
1917+
public import Mathlib.Analysis.Convex.Gradient
19161918
public import Mathlib.Analysis.Convex.Hull
19171919
public import Mathlib.Analysis.Convex.Independent
19181920
public import Mathlib.Analysis.Convex.Integral
19191921
public import Mathlib.Analysis.Convex.Intrinsic
19201922
public import Mathlib.Analysis.Convex.Jensen
19211923
public import Mathlib.Analysis.Convex.Join
19221924
public import Mathlib.Analysis.Convex.KreinMilman
1925+
public import Mathlib.Analysis.Convex.LineDeriv
19231926
public import Mathlib.Analysis.Convex.LinearIsometry
19241927
public import Mathlib.Analysis.Convex.Measure
19251928
public import Mathlib.Analysis.Convex.MetricSpace

‎Mathlib/Analysis/Convex/Deriv.lean‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -603,6 +603,22 @@ lemma deriv_le_slope (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy
603603
deriv f x ≤ slope f x y :=
604604
le_slope_of_hasDerivAt hfc hx hy hxy hfd.hasDerivAt
605605

606+
/-- Additive form of the 1D first-order convexity inequality: for `f : ℝ → ℝ` convex on `S`,
607+
`x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
608+
`f x + f' * (y - x) ≤ f y` where `f' = deriv f x`. -/
609+
lemma add_hasDerivAt_mul_le (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
610+
(ha : HasDerivAt f f' x) :
611+
f x + f' * (y - x) ≤ f y := by
612+
have h := hfc.le_slope_of_hasDerivAt hx hy hxy ha
613+
rw [slope_def_field, le_div_iff₀ (sub_pos.mpr hxy)] at h
614+
linarith
615+
616+
/-- Reformulation of `ConvexOn.add_hasDerivAt_mul_le` using `deriv`. -/
617+
lemma add_deriv_mul_le (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
618+
(hfd : DifferentiableAt ℝ f x) :
619+
f x + deriv f x * (y - x) ≤ f y :=
620+
hfc.add_hasDerivAt_mul_le hx hy hxy hfd.hasDerivAt
621+
606622
end left
607623

608624
section right
@@ -774,6 +790,22 @@ lemma deriv_lt_slope (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S
774790
deriv f x < slope f x y :=
775791
hfc.lt_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt
776792

793+
/-- Strict additive form of the 1D first-order convexity inequality: for `f : ℝ → ℝ` strictly
794+
convex on `S`, `x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
795+
`f x + f' * (y - x) < f y` where `f' = deriv f x`. -/
796+
lemma add_hasDerivAt_mul_lt (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
797+
(ha : HasDerivAt f f' x) :
798+
f x + f' * (y - x) < f y := by
799+
have h := hfc.lt_slope_of_hasDerivAt hx hy hxy ha
800+
rw [slope_def_field, lt_div_iff₀ (sub_pos.mpr hxy)] at h
801+
linarith
802+
803+
/-- Reformulation of `StrictConvexOn.add_hasDerivAt_mul_lt` using `deriv`. -/
804+
lemma add_deriv_mul_lt (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
805+
(hfd : DifferentiableAt ℝ f x) :
806+
f x + deriv f x * (y - x) < f y :=
807+
hfc.add_hasDerivAt_mul_lt hx hy hxy hfd.hasDerivAt
808+
777809
end left
778810

779811
section right
@@ -892,6 +924,22 @@ lemma slope_le_deriv (hfc : ConcaveOn ℝ S f)
892924
slope f x y ≤ deriv f x :=
893925
hfc.slope_le_of_hasDerivAt hx hy hxy hfd.hasDerivAt
894926

927+
/-- Additive form of the 1D first-order concavity inequality: for `f : ℝ → ℝ` concave on `S`,
928+
`x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
929+
`f y ≤ f x + f' * (y - x)` where `f' = deriv f x`. -/
930+
lemma le_add_hasDerivAt_mul (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
931+
(ha : HasDerivAt f f' x) :
932+
f y ≤ f x + f' * (y - x) := by
933+
have h := hfc.slope_le_of_hasDerivAt hx hy hxy ha
934+
rw [slope_def_field, div_le_iff₀ (sub_pos.mpr hxy)] at h
935+
linarith
936+
937+
/-- Reformulation of `ConcaveOn.le_add_hasDerivAt_mul` using `deriv`. -/
938+
lemma le_add_deriv_mul (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
939+
(hfd : DifferentiableAt ℝ f x) :
940+
f y ≤ f x + deriv f x * (y - x) :=
941+
hfc.le_add_hasDerivAt_mul hx hy hxy hfd.hasDerivAt
942+
895943
end left
896944

897945
section right
@@ -992,6 +1040,22 @@ lemma slope_lt_deriv (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈
9921040
slope f x y < deriv f x :=
9931041
hfc.slope_lt_of_hasDerivAt hx hy hxy hfd.hasDerivAt
9941042

1043+
/-- Strict additive form of the 1D first-order concavity inequality: for `f : ℝ → ℝ` strictly
1044+
concave on `S`, `x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
1045+
`f y < f x + f' * (y - x)` where `f' = deriv f x`. -/
1046+
lemma lt_add_hasDerivAt_mul (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
1047+
(ha : HasDerivAt f f' x) :
1048+
f y < f x + f' * (y - x) := by
1049+
have h := hfc.slope_lt_of_hasDerivAt hx hy hxy ha
1050+
rw [slope_def_field, div_lt_iff₀ (sub_pos.mpr hxy)] at h
1051+
linarith
1052+
1053+
/-- Reformulation of `StrictConcaveOn.lt_add_hasDerivAt_mul` using `deriv`. -/
1054+
lemma lt_add_deriv_mul (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
1055+
(hfd : DifferentiableAt ℝ f x) :
1056+
f y < f x + deriv f x * (y - x) :=
1057+
hfc.lt_add_hasDerivAt_mul hx hy hxy hfd.hasDerivAt
1058+
9951059
end left
9961060

9971061
section right

‎Mathlib/Analysis/Convex/FDeriv.lean‎

Lines changed: 157 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
/-
2+
Copyright (c) 2026 Christoph Spiegel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Christoph Spiegel
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.Convex.LineDeriv
9+
public import Mathlib.Analysis.Calculus.FDeriv.Basic
10+
11+
/-!
12+
# First-order convexity inequality via the Fréchet derivative
13+
14+
For `f : E → ℝ` convex on `s ⊆ E` and Fréchet-differentiable at `x ∈ s`, the first-order
15+
convexity inequality
16+
17+
`f x + (fderiv ℝ f x) (y - x) ≤ f y`
18+
19+
holds for `y ∈ s`. This is the Fréchet-derivative restatement of the line-derivative form
20+
in `Mathlib.Analysis.Convex.LineDeriv`, lifted via `HasFDerivAt.hasLineDerivAt`.
21+
22+
The `HasFDerivAt`-flavoured statements are the primitives; the `fderiv`-flavoured ones are
23+
corollaries under `DifferentiableAt`.
24+
25+
## Main results
26+
27+
* `ConvexOn.add_hasFDerivAt_le` / `ConvexOn.add_fderiv_le` — the first-order convexity
28+
inequality (Fréchet form).
29+
* `ConcaveOn.le_add_hasFDerivAt` / `ConcaveOn.le_add_fderiv` — the concave dual.
30+
* `ConvexOn.fderiv_sub_nonneg` — monotonicity along the chord:
31+
`0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x)`.
32+
* `StrictConvexOn.add_hasFDerivAt_lt` / `StrictConvexOn.add_fderiv_lt` — strict variant.
33+
* `StrictConcaveOn.lt_add_hasFDerivAt` / `StrictConcaveOn.lt_add_fderiv` — strict concave dual.
34+
* `ConvexOn.isMinOn_of_fderiv_eq_zero` — convex + zero Fréchet derivative at `x` ⟹ `x`
35+
minimises `f`.
36+
* `convexOn_iff_add_fderiv_le` — iff converse: differentiability plus the first-order
37+
inequality everywhere implies `ConvexOn`.
38+
-/
39+
40+
public section
41+
42+
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
43+
variable {f : E → ℝ} {s : Set E} {x y : E}
44+
45+
namespace ConvexOn
46+
47+
/-- For a convex function `f` with Fréchet derivative `f'` at `x`, the first-order inequality
48+
`f x + f' (y - x) ≤ f y` holds. -/
49+
theorem add_hasFDerivAt_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
50+
{f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
51+
f x + f' (y - x) ≤ f y :=
52+
hc.add_hasLineDerivAt_le hx hy (hf.hasLineDerivAt _)
53+
54+
/-- For a convex function `f` Fréchet-differentiable at `x`, the first-order inequality
55+
`f x + (fderiv ℝ f x) (y - x) ≤ f y` holds. -/
56+
theorem add_fderiv_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
57+
(hf : DifferentiableAt ℝ f x) :
58+
f x + fderiv ℝ f x (y - x) ≤ f y :=
59+
hc.add_hasFDerivAt_le hx hy hf.hasFDerivAt
60+
61+
/-- Monotonicity of the Fréchet derivative along the chord: for convex `f` differentiable
62+
at `x` and `y`, `0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x)`. -/
63+
theorem fderiv_sub_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
64+
(hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
65+
0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x) := by
66+
rw [ContinuousLinearMap.sub_apply, ← hfx.lineDeriv_eq_fderiv, ← hfy.lineDeriv_eq_fderiv]
67+
exact hc.lineDeriv_sub_nonneg hx hy hfx.lineDifferentiableAt hfy.lineDifferentiableAt
68+
69+
/-- A convex function with a vanishing Fréchet derivative at an interior point of differentiability
70+
attains its minimum there. -/
71+
theorem isMinOn_of_fderiv_eq_zero (hc : ConvexOn ℝ s f) (hx : x ∈ s)
72+
(hf : DifferentiableAt ℝ f x) (hgrad : fderiv ℝ f x = 0) :
73+
IsMinOn f s x :=
74+
fun y hy => by simpa [hgrad] using hc.add_fderiv_le hx hy hf
75+
76+
end ConvexOn
77+
78+
namespace ConcaveOn
79+
80+
/-- For a concave function `f` with Fréchet derivative `f'` at `x`, the reverse first-order
81+
inequality `f y ≤ f x + f' (y - x)` holds. -/
82+
theorem le_add_hasFDerivAt (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
83+
{f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
84+
f y ≤ f x + f' (y - x) :=
85+
hc.le_add_hasLineDerivAt hx hy (hf.hasLineDerivAt _)
86+
87+
/-- For a concave function `f` Fréchet-differentiable at `x`, the reverse first-order
88+
inequality `f y ≤ f x + (fderiv ℝ f x) (y - x)` holds. -/
89+
theorem le_add_fderiv (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
90+
(hf : DifferentiableAt ℝ f x) :
91+
f y ≤ f x + fderiv ℝ f x (y - x) :=
92+
hc.le_add_hasFDerivAt hx hy hf.hasFDerivAt
93+
94+
end ConcaveOn
95+
96+
namespace StrictConvexOn
97+
98+
/-- Strict variant of the first-order inequality for strictly convex `f` with Fréchet derivative
99+
`f'` at `x`, assuming `x ≠ y`: `f x + f' (y - x) < f y`. -/
100+
theorem add_hasFDerivAt_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
101+
{f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
102+
f x + f' (y - x) < f y :=
103+
hc.add_hasLineDerivAt_lt hx hy hxy (hf.hasLineDerivAt _)
104+
105+
/-- Strict variant of the first-order inequality for strictly convex `f`:
106+
when `x ≠ y`, the inequality is strict. -/
107+
theorem add_fderiv_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
108+
(hf : DifferentiableAt ℝ f x) :
109+
f x + fderiv ℝ f x (y - x) < f y :=
110+
hc.add_hasFDerivAt_lt hx hy hxy hf.hasFDerivAt
111+
112+
end StrictConvexOn
113+
114+
namespace StrictConcaveOn
115+
116+
/-- Strict variant of the reverse first-order inequality for strictly concave `f` with Fréchet
117+
derivative `f'` at `x`, assuming `x ≠ y`: `f y < f x + f' (y - x)`. -/
118+
theorem lt_add_hasFDerivAt (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
119+
{f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
120+
f y < f x + f' (y - x) :=
121+
hc.lt_add_hasLineDerivAt hx hy hxy (hf.hasLineDerivAt _)
122+
123+
/-- Strict variant of the reverse first-order inequality for strictly concave `f`: when `x ≠ y`,
124+
the inequality is strict. -/
125+
theorem lt_add_fderiv (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
126+
(hf : DifferentiableAt ℝ f x) :
127+
f y < f x + fderiv ℝ f x (y - x) :=
128+
hc.lt_add_hasFDerivAt hx hy hxy hf.hasFDerivAt
129+
130+
end StrictConcaveOn
131+
132+
/-- A differentiable function is convex iff it satisfies the first-order inequality
133+
at every pair of points in `s`. -/
134+
theorem convexOn_iff_add_fderiv_le (hs : Convex ℝ s) (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) :
135+
ConvexOn ℝ s f ↔
136+
∀ x ∈ s, ∀ y ∈ s, f x + fderiv ℝ f x (y - x) ≤ f y := by
137+
refine ⟨fun hc x hx y hy => hc.add_fderiv_le hx hy (hf x hx), fun H => ⟨hs, ?_⟩⟩
138+
intro x hx y hy a b ha hb hab
139+
set z := a • x + b • y with hz
140+
set L := fderiv ℝ f z (x - y) with hL
141+
change f z ≤ a • f x + b • f y
142+
simp only [smul_eq_mul]
143+
have hzs : z ∈ s := hs hx hy ha hb hab
144+
have hb_eq : b = 1 - a := by linarith
145+
have hxz : x - z = b • (x - y) := by rw [hz, hb_eq]; module
146+
have hyz : y - z = -(a • (x - y)) := by rw [hz, hb_eq]; module
147+
have hzx : f z + b * L ≤ f x := by
148+
have h := H z hzs x hx
149+
rwa [hxz, (fderiv ℝ f z).map_smul, smul_eq_mul] at h
150+
have hzy : f z - a * L ≤ f y := by
151+
have h := H z hzs y hy
152+
rw [hyz, map_neg, (fderiv ℝ f z).map_smul, smul_eq_mul] at h
153+
linarith
154+
calc f z
155+
= a * (f z + b * L) + b * (f z - a * L) := by linear_combination (f z) * hab.symm
156+
_ ≤ a * f x + b * f y :=
157+
add_le_add (mul_le_mul_of_nonneg_left hzx ha) (mul_le_mul_of_nonneg_left hzy hb)

‎Mathlib/Analysis/Convex/Gradient.lean‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
/-
2+
Copyright (c) 2026 Christoph Spiegel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Christoph Spiegel
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.Convex.FDeriv
9+
public import Mathlib.Analysis.Calculus.Gradient.Basic
10+
11+
/-!
12+
# First-order convexity inequality via the gradient
13+
14+
On a Hilbert space `F`, for `f : F → ℝ` convex on `s ⊆ F` and differentiable at `x ∈ s`,
15+
the first-order convexity inequality
16+
17+
`f x + ⟪∇ f x, y - x⟫ ≤ f y`
18+
19+
holds for `y ∈ s`. This is the gradient/inner-product restatement of the Fréchet form
20+
in `Mathlib.Analysis.Convex.FDeriv`, lifted via Riesz representation
21+
(`inner_gradient_left`).
22+
23+
## Main results
24+
25+
* `ConvexOn.add_inner_gradient_le` — the first-order convexity inequality (gradient form).
26+
* `ConcaveOn.le_add_inner_gradient` — the concave dual.
27+
* `ConvexOn.inner_gradient_sub_nonneg` — monotonicity along the chord:
28+
`0 ≤ ⟪∇ f y - ∇ f x, y - x⟫`.
29+
* `ConvexOn.isMinOn_of_gradient_eq_zero` — convex + zero gradient at `x` ⟹ `x` minimises `f`.
30+
* `StrictConvexOn.add_inner_gradient_lt` — strict variant.
31+
* `StrictConcaveOn.lt_add_inner_gradient` — strict concave dual.
32+
* `convexOn_iff_add_inner_gradient_le` — iff converse.
33+
-/
34+
35+
public section
36+
37+
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
38+
variable {f : F → ℝ} {s : Set F} {x y : F}
39+
40+
open InnerProductSpace
41+
open scoped Gradient RealInnerProductSpace
42+
43+
namespace ConvexOn
44+
45+
/-- For a convex function `f` differentiable at `x` on a Hilbert space, the first-order
46+
inequality `f x + ⟪∇ f x, y - x⟫ ≤ f y` holds. -/
47+
theorem add_inner_gradient_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
48+
(hf : DifferentiableAt ℝ f x) :
49+
f x + ⟪∇ f x, y - x⟫ ≤ f y := by
50+
rw [inner_gradient_left]
51+
exact hc.add_fderiv_le hx hy hf
52+
53+
/-- Monotonicity of the gradient along the chord: for convex `f` differentiable at `x`
54+
and `y`, `0 ≤ ⟪∇ f y - ∇ f x, y - x⟫`. -/
55+
theorem inner_gradient_sub_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
56+
(hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
57+
0 ≤ ⟪∇ f y - ∇ f x, y - x⟫ := by
58+
rw [inner_sub_left, inner_gradient_left, inner_gradient_left,
59+
← ContinuousLinearMap.sub_apply]
60+
exact hc.fderiv_sub_nonneg hx hy hfx hfy
61+
62+
/-- A convex function attains its minimum on `s` at any critical point: if `f` is convex on
63+
`s`, Fréchet-differentiable at `x ∈ s`, and `∇ f x = 0`, then `x` minimizes `f` on `s`.
64+
Multi-dimensional gradient analogue of `ConvexOn.isMinOn_of_rightDeriv_eq_zero`. -/
65+
theorem isMinOn_of_gradient_eq_zero (hc : ConvexOn ℝ s f) (hx : x ∈ s)
66+
(hf : DifferentiableAt ℝ f x) (hg : ∇ f x = 0) :
67+
IsMinOn f s x := fun _ hy => by
68+
simpa [hg] using hc.add_inner_gradient_le hx hy hf
69+
70+
end ConvexOn
71+
72+
namespace ConcaveOn
73+
74+
/-- For a concave function `f` differentiable at `x` on a Hilbert space, the reverse
75+
first-order inequality `f y ≤ f x + ⟪∇ f x, y - x⟫` holds. -/
76+
theorem le_add_inner_gradient (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
77+
(hf : DifferentiableAt ℝ f x) :
78+
f y ≤ f x + ⟪∇ f x, y - x⟫ := by
79+
rw [inner_gradient_left]
80+
exact hc.le_add_fderiv hx hy hf
81+
82+
end ConcaveOn
83+
84+
namespace StrictConvexOn
85+
86+
/-- Strict variant of the first-order gradient inequality for strictly convex `f`. -/
87+
theorem add_inner_gradient_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
88+
(hxy : x ≠ y) (hf : DifferentiableAt ℝ f x) :
89+
f x + ⟪∇ f x, y - x⟫ < f y := by
90+
rw [inner_gradient_left]
91+
exact hc.add_fderiv_lt hx hy hxy hf
92+
93+
end StrictConvexOn
94+
95+
namespace StrictConcaveOn
96+
97+
/-- Strict variant of the reverse first-order gradient inequality for strictly concave `f`. -/
98+
theorem lt_add_inner_gradient (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
99+
(hxy : x ≠ y) (hf : DifferentiableAt ℝ f x) :
100+
f y < f x + ⟪∇ f x, y - x⟫ := by
101+
rw [inner_gradient_left]
102+
exact hc.lt_add_fderiv hx hy hxy hf
103+
104+
end StrictConcaveOn
105+
106+
/-- A differentiable function on a Hilbert space is convex iff it satisfies the first-order
107+
gradient inequality at every pair of points in `s`. -/
108+
theorem convexOn_iff_add_inner_gradient_le (hs : Convex ℝ s)
109+
(hf : ∀ x ∈ s, DifferentiableAt ℝ f x) :
110+
ConvexOn ℝ s f ↔ ∀ x ∈ s, ∀ y ∈ s, f x + ⟪∇ f x, y - x⟫ ≤ f y := by
111+
rw [convexOn_iff_add_fderiv_le hs hf]
112+
refine forall_congr' fun _ => imp_congr_right fun _ => forall_congr' fun _ =>
113+
imp_congr_right fun _ => ?_
114+
rw [inner_gradient_left]

0 commit comments

Comments
 (0)