feat(Analysis/Calculus/LipschitzSmooth): Baillon-Haddad theorem and convex equivalences#29
Closed
FordUniver wants to merge 1 commit into
Closed
Conversation
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
9fe85d4 to
ba1c53b
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
33286ed to
13c90a0
Compare
2 tasks
FordUniver
changed the title
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
ba1c53b to
39d8d0d
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
13c90a0 to
4cc2fb9
Compare
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
39d8d0d to
3153be4
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
4cc2fb9 to
f1edef3
Compare
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
3153be4 to
505b919
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
f1edef3 to
cb27faf
Compare
FordUniver
changed the title
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
505b919 to
db88c49
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
cb27faf to
c43b298
Compare
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
db88c49 to
79ba04f
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
2 times, most recently
from
586f76e to
bc531ef
Compare
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
79ba04f to
64bb11c
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
bc531ef to
d3ec459
Compare
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
64bb11c to
99712f3
Compare
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
d3ec459 to
9b128f3
Compare
…alences For a differentiable convex function on a Hilbert space, `K`-smoothness implies `K`-cocoercivity of the gradient (`ConvexOn.cocoerciveWith_of_lipschitzSmoothWith`). Combined with the descent lemma and the elementary cocoercive ⟹ Lipschitz-gradient direction, this yields the four pairwise iff equivalences between `LipschitzSmoothWith`, `LipschitzWith (fderiv ℝ f)`, `LipschitzWith (∇ f)`, and `CocoerciveWith` under `ConvexOn ℝ Set.univ f` and `Differentiable ℝ f`.
FordUniver
force-pushed
the
feat/lipschitzSmooth-convex
branch
from
9b128f3 to
5ef2369
Compare
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
99712f3 to
d9e8bb5
Compare
FordUniver
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
For a differentiable convex function on a Hilbert space, the Baillon-Haddad theorem identifies
K-smoothness withK-cocoercivity of the gradient. This closes the four-way equivalence betweenLipschitzSmoothWith K f,LipschitzWith K (fderiv ℝ f),LipschitzWith K (∇ f), andCocoerciveWith K funderConvexOn ℝ Set.univ f.The textbook proof goes through the auxiliary function
φₓ(z) := f(z) - ⟨∇f(x), z⟩(convex,K-smooth, minimum atx) while here the argument is inlined without constructingφₓ. I am considering adding anAlgebrafile toLipschitzSmoothWithin a future PR that would allow to factor the proof throughφₓexplicitly, but I don't think it is strictly necessary and I am not sure yet about the uses beyond a more idiomatic proof here.LipschitzSmoothWithandCocoerciveWithleanprover-community/mathlib4#39574AffineMap.lineMapleanprover-community/mathlib4#39206inner_gradientlemmas leanprover-community/mathlib4#39203toDual_gradientand companions leanprover-community/mathlib4#39202Diff: link