Skip to content

Commit 608f5bb

Browse files
FordUniverFordUniver
committed
feat(Analysis/Calculus/LipschitzSmooth): add descent lemma
Adds the descent lemma in Fréchet / 1D `deriv` / Hilbert gradient form on top of the foundational `LipschitzSmoothWith` API: a differentiable function whose derivative (in any form) is `K`-Lipschitz is `K`-smooth. The proof routes through a segment-pointwise predicate `LipschitzSmoothOnSegmentWith` and the fundamental theorem of calculus along a line segment. Includes the Riesz isomorphism between Fréchet and gradient forms for Lipschitz constants and its 1D analogue.
1 parent 4b144de commit 608f5bb

3 files changed

Lines changed: 119 additions & 0 deletions

File tree

‎Mathlib/Analysis/Calculus/LipschitzSmooth/Deriv.lean‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,3 +68,26 @@ theorem deriv_sub_mul_le (h : LipschitzSmoothWith K f) (x y : ℝ)
6868
end Real
6969

7070
end LipschitzSmoothWith
71+
72+
/-! ### Lipschitz constants of `fderiv` versus `deriv` -/
73+
74+
section Real
75+
76+
variable {f : ℝ → ℝ}
77+
78+
/-- For `f : ℝ → ℝ`, the Lipschitz constants of `fderiv ℝ f` and `deriv f` coincide:
79+
`deriv f` is the composition of `fderiv ℝ f` with the isometry
80+
`(ContinuousLinearMap.toSpanSingletonLIE ℝ ℝ).symm` (evaluation at `1`). -/
81+
theorem lipschitzWith_fderiv_iff_lipschitzWith_deriv :
82+
LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (deriv f) :=
83+
((ContinuousLinearMap.toSpanSingletonLIE ℝ ℝ).symm.isometry.lipschitzWith_iff K).symm
84+
85+
/-! ### Descent lemma (1D) -/
86+
87+
/-- **Descent lemma (1D).** If `f : ℝ → ℝ` is differentiable and its derivative is
88+
`K`-Lipschitz, then `f` is `K`-smooth. -/
89+
theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith_deriv
90+
(hf : Differentiable ℝ f) (hL : LipschitzWith K (deriv f)) : LipschitzSmoothWith K f :=
91+
hf.lipschitzSmoothWith_of_lipschitzWith (lipschitzWith_fderiv_iff_lipschitzWith_deriv.mpr hL)
92+
93+
end Real

‎Mathlib/Analysis/Calculus/LipschitzSmooth/FDeriv.lean‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,9 @@ module
77

88
public import Mathlib.Analysis.Calculus.FDeriv.Basic
99
public import Mathlib.Analysis.Calculus.LipschitzSmooth.Basic
10+
public import Mathlib.Analysis.Normed.Affine.AddTorsor
11+
public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
12+
public import Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
1013

1114
/-!
1215
# Lipschitz smoothness via the Fréchet derivative
@@ -16,6 +19,11 @@ Fréchet-derivative restatements of the `LipschitzSmoothWith` predicate for
1619
pointwise, and the predicate is equivalent to the two-sided Taylor bound stated
1720
in `fderiv` form. The one-sided descent bounds require an order on the codomain
1821
and are stated for real-valued `f` in a dedicated section.
22+
23+
This file also defines the segment-pointwise predicate `LipschitzSmoothOnSegmentWith` and
24+
proves the **descent lemma**: a differentiable function with `K`-Lipschitz Fréchet derivative
25+
is `K`-smooth. The proof integrates the segment-pointwise norm-bound along the segment from
26+
`x` to `y` using the fundamental theorem of calculus.
1927
-/
2028

2129
public section
@@ -74,3 +82,73 @@ theorem fderiv_sub_apply_le (h : LipschitzSmoothWith K f) (x y : E)
7482
end Real
7583

7684
end LipschitzSmoothWith
85+
86+
/-! ### Descent lemma -/
87+
88+
open AffineMap MeasureTheory
89+
90+
/-- The pointwise two-sided Lipschitz-smoothness bound on the Fréchet derivative along the
91+
segment from `x` to `y`: `‖(fderiv ℝ f z - fderiv ℝ f x) (y - x)‖ ≤ K · dist x z · dist x y`
92+
for all `z ∈ [x -[ℝ] y]`. This is the segment-pointwise form that integrates to the descent
93+
inequality. -/
94+
abbrev LipschitzSmoothOnSegmentWith (K : NNReal) (f : E → F) : Prop :=
95+
∀ x y : E, ∀ z ∈ segment ℝ x y,
96+
‖(fderiv ℝ f z - fderiv ℝ f x) (y - x)‖ ≤ K * dist x z * dist x y
97+
98+
/-- A `K`-Lipschitz Fréchet derivative implies the segment-pointwise smoothness bound.
99+
Direct from the operator-norm bound (`ContinuousLinearMap.le_opNorm`) plus the Lipschitz bound
100+
at the pair `(z, x)`. -/
101+
theorem LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv
102+
(hL : LipschitzWith K (fderiv ℝ f)) : LipschitzSmoothOnSegmentWith K f := fun x y z _ =>
103+
calc ‖(fderiv ℝ f z - fderiv ℝ f x) (y - x)‖
104+
≤ ‖fderiv ℝ f z - fderiv ℝ f x‖ * ‖y - x‖ := ContinuousLinearMap.le_opNorm _ _
105+
_ = dist (fderiv ℝ f x) (fderiv ℝ f z) * dist x y := by simp only [← dist_eq_norm']
106+
_ ≤ K * dist x z * dist x y := mul_le_mul_of_nonneg_right (hL.dist_le_mul _ _) dist_nonneg
107+
108+
/-- For a segment-pointwise Lipschitz-smooth function with continuous Fréchet derivative, the
109+
norm of the curve integral of `fderiv ℝ f z - fderiv ℝ f x` along the segment is
110+
bounded by `K/2 · (dist x y)²`. The quantitative FTC step of the descent lemma. -/
111+
theorem LipschitzSmoothOnSegmentWith.curveIntegral_norm_le
112+
(h : LipschitzSmoothOnSegmentWith K f) (hcont : Continuous (fderiv ℝ f)) (x y : E) :
113+
‖∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x)‖ ≤ K / 2 * (dist x y) ^ 2 := by
114+
have h_integrable : IntervalIntegrable
115+
(fun t => (fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x)) volume 0 1 :=
116+
curveIntegrable_segment.mp <|
117+
(hcont.curveIntegrable_segment).sub (curveIntegrable_segment_const _ x y)
118+
calc ‖∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x)‖
119+
_ = ‖∫ t in (0:ℝ)..1, (fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x)‖ := by
120+
rw [curveIntegral_segment]
121+
_ ≤ ∫ t in (0:ℝ)..1, ‖(fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x)‖ :=
122+
intervalIntegral.norm_integral_le_integral_norm zero_le_one
123+
_ ≤ ∫ t in (0:ℝ)..1, K * (dist x y) ^ 2 * t :=
124+
intervalIntegral.integral_mono_on zero_le_one h_integrable.norm
125+
(Continuous.intervalIntegrable (by fun_prop) _ _) (fun t ht =>
126+
(h _ _ _ (segment_eq_image_lineMap ℝ x y ▸ Set.mem_image_of_mem _ ht)).trans_eq <| by
127+
rw [dist_left_lineMap, Real.norm_of_nonneg ht.1]; ring)
128+
_ = K * (dist x y) ^ 2 * ∫ t in (0:ℝ)..1, t := intervalIntegral.integral_const_mul _ _
129+
_ = K / 2 * (dist x y) ^ 2 := by rw [integral_id]; ring
130+
131+
/-- The segment-pointwise smoothness bound, together with differentiability and continuity of
132+
the Fréchet derivative, implies `K`-smoothness. The proof integrates the pointwise norm bound
133+
along the segment from `x` to `y` using FTC. -/
134+
theorem LipschitzSmoothOnSegmentWith.lipschitzSmoothWith [CompleteSpace F]
135+
(hptwise : LipschitzSmoothOnSegmentWith K f) (hf : Differentiable ℝ f)
136+
(hcont : Continuous (fderiv ℝ f)) : LipschitzSmoothWith K f := by
137+
refine lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => ?_
138+
have heq : f y - f x - lineDeriv ℝ f x (y - x) =
139+
∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x) := calc
140+
_ = f y - f x - (fderiv ℝ f x) (y - x) := by rw [(hf x).lineDeriv_eq_fderiv]
141+
_ = (∫ᶜ z in .segment x y, fderiv ℝ f z) - ∫ᶜ _ in .segment x y, fderiv ℝ f x := by
142+
rw [← curveIntegral_fderiv_segment (fun z _ => hf z) hcont.continuousOn,
143+
← curveIntegral_segment_const]
144+
_ = ∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x) :=
145+
(curveIntegral_fun_sub (hcont.curveIntegrable_segment)
146+
(curveIntegrable_segment_const _ x y)).symm
147+
rw [heq]
148+
exact hptwise.curveIntegral_norm_le hcont x y
149+
150+
/-- **Descent lemma.** If `f` is differentiable and its Fréchet derivative is
151+
`K`-Lipschitz, then `f` is `K`-smooth (without convexity assumption). -/
152+
theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith [CompleteSpace F]
153+
(hf : Differentiable ℝ f) (hL : LipschitzWith K (fderiv ℝ f)) : LipschitzSmoothWith K f :=
154+
(LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv hL).lipschitzSmoothWith hf hL.continuous

‎Mathlib/Analysis/Calculus/LipschitzSmooth/Gradient.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ public section
2626
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
2727
variable {K : NNReal} {f : F → ℝ}
2828

29+
open InnerProductSpace
2930
open scoped Gradient RealInnerProductSpace
3031

3132
theorem lipschitzSmoothWith_iff_inner_gradient (hf : Differentiable ℝ f) :
@@ -78,3 +79,20 @@ theorem CocoerciveWith.lipschitzWith_gradient (h : CocoerciveWith K f) : Lipschi
7879
simp only [dist_eq_norm']
7980
nlinarith [h x y, mul_nonneg K.coe_nonneg (norm_nonneg (y - x)),
8081
mul_le_mul_of_nonneg_left (real_inner_le_norm (∇ f y - ∇ f x) (y - x)) K.coe_nonneg]
82+
83+
/-! ### Riesz isomorphism for Lipschitz constants -/
84+
85+
/-- The Riesz isomorphism identifies the Lipschitz constant of the Fréchet derivative with
86+
that of the gradient: `LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f)`. Unconditional —
87+
the gradient is *defined* via Riesz from the fderiv, and Riesz is an isometry. -/
88+
theorem lipschitzWith_fderiv_iff_lipschitzWith_gradient :
89+
LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f) :=
90+
toDual_comp_gradient (𝕜 := ℝ) (f := f) ▸ (toDual ℝ F).isometry.lipschitzWith_iff K
91+
92+
/-! ### Descent lemma (Hilbert form) -/
93+
94+
/-- **Descent lemma (Hilbert form).** If `f : F → ℝ` is differentiable on a Hilbert space
95+
and its gradient `∇ f` is `K`-Lipschitz, then `f` is `K`-smooth. -/
96+
theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith_gradient
97+
(hf : Differentiable ℝ f) (hL : LipschitzWith K (∇ f)) : LipschitzSmoothWith K f :=
98+
hf.lipschitzSmoothWith_of_lipschitzWith (lipschitzWith_fderiv_iff_lipschitzWith_gradient.mpr hL)

0 commit comments

Comments
 (0)