Skip to content

Commit 176036e

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 4e0cf67 commit 176036e

3 files changed

Lines changed: 116 additions & 0 deletions

File tree

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,3 +46,28 @@ theorem deriv_sub_mul_le (h : LipschitzSmoothWith K f) (x y : ℝ)
4646
dist_comm, Real.dist_eq, sq_abs] at this
4747

4848
end LipschitzSmoothWith
49+
50+
/-! ### Riesz isomorphism for 1D Lipschitz constants -/
51+
52+
/-- For `f : ℝ → ℝ`, the Lipschitz constants of `fderiv ℝ f` and `deriv f` coincide.
53+
The isomorphism `r ↦ smulRight 1 r : ℝ → ℝ →L[ℝ] ℝ` is an isometry, so Lipschitz
54+
properties transfer between the two views of the derivative. -/
55+
theorem lipschitzWith_fderiv_iff_lipschitzWith_deriv :
56+
LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (deriv f) := by
57+
have h : ∀ x y : ℝ, fderiv ℝ f x - fderiv ℝ f y =
58+
ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) (deriv f x - deriv f y) := fun x y => by
59+
ext
60+
rw [ContinuousLinearMap.sub_apply, fderiv_eq_deriv_mul, fderiv_eq_deriv_mul,
61+
ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
62+
ring
63+
simp_rw [lipschitzWith_iff_dist_le_mul, dist_eq_norm]
64+
refine forall_congr' fun x => forall_congr' fun y => ?_
65+
rw [h x y, ContinuousLinearMap.norm_smulRight_apply, norm_one, one_mul]
66+
67+
/-! ### Descent lemma (1D) -/
68+
69+
/-- **Descent lemma (1D).** If `f : ℝ → ℝ` is differentiable and its derivative is
70+
`K`-Lipschitz, then `f` is `K`-smooth. -/
71+
theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith_deriv
72+
(hf : Differentiable ℝ f) (hL : LipschitzWith K (deriv f)) : LipschitzSmoothWith K f :=
73+
hf.lipschitzSmoothWith_of_lipschitzWith (lipschitzWith_fderiv_iff_lipschitzWith_deriv.mpr hL)

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

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,21 @@ 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
1316
1417
Fréchet-derivative restatements of the `LipschitzSmoothWith` predicate. For differentiable
1518
`f`, `lineDeriv ℝ f x v = fderiv ℝ f x v` pointwise, and the predicate is equivalent to
1619
the corresponding descent inequality stated in `fderiv` form.
20+
21+
This file also defines the segment-pointwise predicate `LipschitzSmoothOnSegmentWith` and
22+
proves the **descent lemma**: a differentiable function with `K`-Lipschitz Fréchet derivative
23+
is `K`-smooth. The proof integrates the segment-pointwise bound along the segment from `x`
24+
to `y` using the fundamental theorem of calculus.
1725
-/
1826

1927
public section
@@ -47,3 +55,68 @@ theorem fderiv_sub_apply_le (h : LipschitzSmoothWith K f) (x y : F)
4755
exact h.fderiv_apply_sub_le x y hfx hfy
4856

4957
end LipschitzSmoothWith
58+
59+
/-! ### Descent lemma -/
60+
61+
open AffineMap MeasureTheory
62+
63+
/-- The pointwise Lipschitz-smoothness bound on the Fréchet derivative along the segment from
64+
`x` to `y`: `(fderiv ℝ f z - fderiv ℝ f x) (y - x) ≤ K · dist x z · dist x y` for all
65+
`z ∈ [x -[ℝ] y]`. This is the segment-pointwise form that integrates to the descent inequality. -/
66+
abbrev LipschitzSmoothOnSegmentWith (K : NNReal) (f : F → ℝ) : Prop :=
67+
∀ x y : F, ∀ z ∈ segment ℝ x y,
68+
(fderiv ℝ f z - fderiv ℝ f x) (y - x) ≤ ↑K * dist x z * dist x y
69+
70+
/-- A `K`-Lipschitz Fréchet derivative implies the segment-pointwise smoothness bound:
71+
`(fderiv ℝ f z - fderiv ℝ f x) (y - x) ≤ K · dist x z · dist x y` for every `z ∈ [x -[ℝ] y]`.
72+
The argument is Cauchy-Schwarz / `le_opNorm` plus the Lipschitz bound at the pair `(z, x)`. -/
73+
theorem LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv
74+
(hL : LipschitzWith K (fderiv ℝ f)) : LipschitzSmoothOnSegmentWith K f := fun x y z _ =>
75+
calc (fderiv ℝ f z - fderiv ℝ f x) (y - x)
76+
≤ ‖fderiv ℝ f z - fderiv ℝ f x‖ * ‖y - x‖ :=
77+
(Real.le_norm_self _).trans (ContinuousLinearMap.le_opNorm _ _)
78+
_ = dist (fderiv ℝ f x) (fderiv ℝ f z) * dist x y := by repeat rw [← dist_eq_norm']
79+
_ ≤ ↑K * dist x z * dist x y := mul_le_mul_of_nonneg_right (hL.dist_le_mul _ _) dist_nonneg
80+
81+
/-- For a segment-pointwise Lipschitz-smooth function with continuous Fréchet derivative, the
82+
curve integral of `fderiv ℝ f z - fderiv ℝ f x` along the segment from `x` to `y` is bounded
83+
by `K/2 · (dist x y)²`. The quantitative FTC step of the descent lemma. -/
84+
theorem LipschitzSmoothOnSegmentWith.curveIntegral_le
85+
(h : LipschitzSmoothOnSegmentWith K f) (hcont : Continuous (fderiv ℝ f)) (x y : F) :
86+
∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x) ≤ ↑K / 2 * (dist x y) ^ 2 :=
87+
calc ∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x)
88+
_ = ∫ t in 0..1, (fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x) :=
89+
curveIntegral_segment _ _ _
90+
_ ≤ ∫ t in 0..1, ↑K * (dist x y) ^ 2 * t :=
91+
intervalIntegral.integral_mono_on (by norm_num)
92+
(curveIntegrable_segment.mp <|
93+
(hcont.curveIntegrable_segment).sub (curveIntegrable_segment_const _ x y))
94+
(Continuous.intervalIntegrable (by fun_prop) _ _) (fun t ht =>
95+
(h _ _ _ (segment_eq_image_lineMap ℝ x y ▸ Set.mem_image_of_mem _ ht)).trans_eq <| by
96+
rw [dist_left_lineMap, Real.norm_of_nonneg ht.1]; ring)
97+
_ = ↑K * (dist x y) ^ 2 * ∫ t in 0..1, t := intervalIntegral.integral_const_mul _ _
98+
_ = ↑K / 2 * (dist x y) ^ 2 := by rw [integral_id]; ring
99+
100+
/-- The segment-pointwise smoothness bound, together with differentiability and continuity of
101+
the Fréchet derivative, implies `K`-smoothness. The proof integrates the pointwise bound
102+
`K · dist x z · dist x y` along the segment from `x` to `y` using FTC. -/
103+
theorem LipschitzSmoothOnSegmentWith.lipschitzSmoothWith
104+
(hptwise : LipschitzSmoothOnSegmentWith K f) (hf : Differentiable ℝ f)
105+
(hcont : Continuous (fderiv ℝ f)) : LipschitzSmoothWith K f := by
106+
refine lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => ?_
107+
have := calc f y - f x - lineDeriv ℝ f x (y - x)
108+
_ = f y - f x - (fderiv ℝ f x) (y - x) := by rw [(hf x).lineDeriv_eq_fderiv]
109+
_ = (∫ᶜ z in .segment x y, fderiv ℝ f z) - ∫ᶜ _ in .segment x y, fderiv ℝ f x := by
110+
rw [← curveIntegral_fderiv_segment (fun z _ => hf z) hcont.continuousOn,
111+
← curveIntegral_segment_const]
112+
_ = ∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x) :=
113+
(curveIntegral_fun_sub (hcont.curveIntegrable_segment)
114+
(curveIntegrable_segment_const _ x y)).symm
115+
_ ≤ ↑K / 2 * dist x y ^ 2 := hptwise.curveIntegral_le hcont x y
116+
linarith
117+
118+
/-- **Descent lemma.** If `f` is differentiable and its Fréchet derivative is
119+
`K`-Lipschitz, then `f` is `K`-smooth (without convexity assumption). -/
120+
theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith
121+
(hf : Differentiable ℝ f) (hL : LipschitzWith K (fderiv ℝ f)) : LipschitzSmoothWith K f :=
122+
(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) :
@@ -66,3 +67,20 @@ theorem CocoerciveWith.lipschitzWith_gradient (h : CocoerciveWith K f) : Lipschi
6667
simp only [dist_eq_norm']
6768
nlinarith [h x y, mul_nonneg K.coe_nonneg (norm_nonneg (y - x)),
6869
mul_le_mul_of_nonneg_left (real_inner_le_norm (∇ f y - ∇ f x) (y - x)) K.coe_nonneg]
70+
71+
/-! ### Riesz isomorphism for Lipschitz constants -/
72+
73+
/-- The Riesz isomorphism identifies the Lipschitz constant of the Fréchet derivative with
74+
that of the gradient: `LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f)`. Unconditional —
75+
the gradient is *defined* via Riesz from the fderiv, and Riesz is an isometry. -/
76+
theorem lipschitzWith_fderiv_iff_lipschitzWith_gradient :
77+
LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f) :=
78+
toDual_comp_gradient (𝕜 := ℝ) (f := f) ▸ (toDual ℝ F).isometry.lipschitzWith_iff K
79+
80+
/-! ### Descent lemma (Hilbert form) -/
81+
82+
/-- **Descent lemma (Hilbert form).** If `f : F → ℝ` is differentiable on a Hilbert space
83+
and its gradient `∇ f` is `K`-Lipschitz, then `f` is `K`-smooth. -/
84+
theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith_gradient
85+
(hf : Differentiable ℝ f) (hL : LipschitzWith K (∇ f)) : LipschitzSmoothWith K f :=
86+
hf.lipschitzSmoothWith_of_lipschitzWith (lipschitzWith_fderiv_iff_lipschitzWith_gradient.mpr hL)

0 commit comments

Comments
 (0)