feat(LipschitzSmooth/FiniteDimension): C^{1,1} characterisation in finite dim#34
Closed
FordUniver wants to merge 2 commits into
Closed
feat(LipschitzSmooth/FiniteDimension): C^{1,1} characterisation in finite dim#34FordUniver wants to merge 2 commits into
FordUniver wants to merge 2 commits into
Conversation
FordUniver
force-pushed
the
feat/lipschitzSmooth-basic
branch
from
9437e2a to
6b44bc9
Compare
New file `Mathlib/Analysis/Calculus/LipschitzSmooth/FiniteDimension.lean`
collecting the finite-dim consequences of the two-sided abs predicate:
LipschitzSmoothWith K f ⟹ Differentiable ℝ f
⟹ LipschitzWith K (fderiv ℝ f)
⟹ LocallyLipschitz f
⟹ Continuous f
In finite dim these are equivalences (with the descent lemma supplying
the reverse direction in a sibling file), giving the standard C^{1,1}
characterisation **without any convexity hypothesis on f** — see
Cannarsa-Sinestrari (2004) Corollary 3.3.8 p.61 and Rockafellar-Wets
(1998) Proposition 13.34 p.605. The proofs route through the
K-semiconcavity decomposition `f - K/2 ‖·‖²` concave; without
[FiniteDimensional ℝ F] the result fails (Bauschke-Combettes (2017)
Example 8.42 p.151: discontinuous linear functionals are
LipschitzSmoothWith 0 but not even continuous).
Three proofs are stubbed with `sorry`: `differentiable`,
`lipschitzWith_fderiv`, `locallyLipschitz`. The fourth (`continuous`)
is wired through `locallyLipschitz.continuous` so it will discharge
once `locallyLipschitz` lands.
…llyLipschitz Fill in the first two non-trivial proofs of the finite-dim branch: * `LipschitzSmoothWith.concaveOn_sub_half_sq_norm` — the K-semiconcavity decomposition `f - K/2 ‖·‖²` concave on the whole space. Proof: apply the upper-bound direction of the predicate at `(z, x)` and `(z, y)` with `z = a • x + b • y`, scale by `a, b`, and add; the line-derivative terms cancel by positive homogeneity (since `x - z = b • (x - y)` and `y - z = -a • (x - y)`), the quadratic terms collapse via the parallelogram identity `a‖x‖² + b‖y‖² - ‖a•x + b•y‖² = a b ‖x - y‖²`. Uses `[InnerProductSpace ℝ F]` (no `[FiniteDimensional]`); the parallelogram identity is what restricts to inner-product spaces. * `LipschitzSmoothWith.locallyLipschitz` (under `[FiniteDimensional ℝ F]`) — routes through `concaveOn_sub_half_sq_norm` + mathlib's `ConcaveOn.locallyLipschitz` (which needs finite-dim) for the concave part, plus `(K/2) ‖·‖²` locally Lipschitz via `ContDiff.locallyLipschitz` (since `‖·‖²` is `ContDiff ℝ n` on inner-product spaces). * `LipschitzSmoothWith.continuous` now discharges via `locallyLipschitz.continuous` — no longer `sorry`. * `LipschitzSmoothWith.differentiable` and `lipschitzWith_fderiv` remain `sorry`'d — these are the substantive Cannarsa-Sinestrari 3.3.7/3.3.8 step (super-gradient sandwich + distributional-Hessian operator-norm bound). The proof uses `linear_combination` for the polynomial identities under `a + b = 1` (the parallelogram identity, the coefficient identity `a b² + b a² = a b`, the `(a + b) f z = f z` simplification) and `linarith` for the final inequality assembly; this avoids `nlinarith` search blow-ups on the multiplicative subgoals.
FordUniver
force-pushed
the
feat/lipschitzSmooth-finiteDimension
branch
from
a8c7826 to
1639970
Compare
Owner
Author
|
Superseded by #35 — rescoped to focus on the achievable finite-dim continuity result. The full |
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.
The finite-dim half of the LipschitzSmooth API. Under
[FiniteDimensional ℝ F] [InnerProductSpace ℝ F], the predicate collapses to standardC^{1,1}without any convexity hypothesis (Cannarsa-Sinestrari, Semiconcave Functions (2004), Corollary 3.3.8 p.61). TheFiniteDimensionalhypothesis is necessary, not convenient — discontinuous linear functionals satisfyLipschitzSmoothWith 0 ℓin infinite-dim (Bauschke-Combettes 2017 Example 8.42 p.151).The reverse direction (
LipschitzWith K (fderiv) ⟹ LipschitzSmoothWith K) is the descent lemma and lives infeat/lipschitzSmooth-descent; together they give the convexity-free finite-dim equivalence between the predicate and standardC^{1,1}. Two of the four headline theorems (differentiableandlipschitzWith_fderiv) are currentlysorry'd — these are the substantive Cannarsa-Sinestrari 3.3.7 / 3.3.8 step (super-gradient sandwich + distributional-Hessian operator-norm lift via the parallelogram identity);locallyLipschitzandcontinuousare proven and route through mathlib'sConcaveOn.locallyLipschitzafter the semiconcavity decomposition. The previously sorry'dLipschitzSmoothWith.continuousinBasic.leanof leanprover-community#39574 is removed here; it lives inFiniteDimension.leannow as a corollary with the proper hypothesis. The[InnerProductSpace]restriction (rather than general normed space) is for the parallelogram identity in the decomposition step; a finite-dim-normed-space refinement via norm-equivalence transfer is left as a follow-up. Draft until the two remaining proofs land.LipschitzSmoothWithandCocoerciveWithleanprover-community/mathlib4#39574Diff for the changes just in this PR over its predecessor: link