feat(Analysis/Calculus/LipschitzSmooth): add descent lemma#41495
Open
FordUniver wants to merge 43 commits into
Open
feat(Analysis/Calculus/LipschitzSmooth): add descent lemma#41495FordUniver wants to merge 43 commits into
FordUniver wants to merge 43 commits into
Conversation
The four `inner_gradient[Within]_[left|right]` lemmas in `Mathlib/Analysis/Calculus/Gradient/Basic.lean` required differentiability hypotheses (`DifferentiableAt`, `DifferentiableWithinAt`, plus `UniqueDiffWithinAt` for the `Within` versions). These were never necessary: `gradient` is *defined* via the Riesz isomorphism from `fderiv`, so the identification `⟪∇ f x, y⟫ = fderiv 𝕜 f x y` holds unconditionally — both sides are zero when `f` is not differentiable. Removes the hypotheses and rewrites the proofs to go through `toDual_apply_apply` and `LinearIsometryEquiv.apply_symm_apply` directly. No call-site updates needed (no current mathlib callers pass the now-redundant arguments).
…lineMap Add `AffineMap.lineMap_contDiff_uncurry` (joint smoothness in all three arguments), `AffineMap.lineMap_contDiff` (smoothness in the parameter with fixed endpoints), and the composition family `ContDiff.lineMap`, `ContDiffOn.lineMap`, `ContDiffAt.lineMap`, `ContDiffWithinAt.lineMap`, mirroring the corresponding `Continuous` family in `Mathlib.Topology.Algebra.Affine`. The uncurried and `ContDiffWithinAt` forms are tagged `@[fun_prop]`. Closes the long-standing TODO at `MeasureTheory.Integral.CurveIntegral.Poincare:333` (`-- TODO: add ContDiff.lineMap etc`), where the absence of this API forced a manual `simp only [AffineMap.lineMap_apply_module]` unfold before `fun_prop` could close the goal. The Poincare proof now closes with just `fun_prop` once the new file is imported.
…icate Introduces LipschitzSmoothWith K f for a real-valued function f on a normed real vector space: the quadratic descent inequality f y le f x + lineDeriv R f x (y - x) + (K / 2) (dist x y)^2 stated in line-derivative form so that it does not presuppose Frechet differentiability. The K / 2 convention makes the descent lemma constant-preserving (a K-Lipschitz Frechet derivative gives K-smoothness). Two basic consequences fall directly out of the definition: * LipschitzSmoothWith.lineDeriv_apply_sub_le - the quadratic variation bound on the line-derivative. * LipschitzSmoothWith.lineDeriv_sub_apply_le - function-subtraction form. Frechet- and gradient-form restatements (the actual descent lemma) and the Baillon-Haddad equivalence with cocoercivity under convexity are deferred to follow-up files.
…Deriv layer Adopt the opaque-with-iff pattern for LipschitzSmoothWith: drop the @[expose] annotation so that lineDeriv is treated as an internal implementation detail of the predicate, and provide explicit characterisations and extractors via named API lemmas. Users in any derivative framework reach the predicate through their preferred form via the appropriate iff. Basic.lean changes: * Add lipschitzSmoothWith_iff_lineDeriv (iff characterisation in lineDeriv form, Iff.rfl since the file owns the definition). * Add LipschitzSmoothWith.lineDeriv_descent_le as the named extractor. * Drop @[expose] from the def. FDeriv.lean (new file): * lipschitzSmoothWith_iff_fderiv: iff characterisation in fderiv form under Differentiable. * LipschitzSmoothWith.fderiv_descent_le: descent inequality extractor in fderiv form. * LipschitzSmoothWith.fderiv_apply_sub_le and fderiv_sub_apply_le: variance bound on the Frechet derivative in applied and function-subtraction forms. The Frechet-form descent lemma proper (converse direction, requires segment-level FTC machinery) is deferred to a follow-up.
Mirrors the FDeriv-layer pattern (iff characterisation + extractor + variance bound) for the 1D-deriv and Hilbert-gradient flavours of the LipschitzSmoothWith predicate, completing the four derivative-form characterisations symmetrically. Deriv.lean: * lipschitzSmoothWith_iff_deriv: characterisation for f : R -> R in deriv form under Differentiable, with the (y - x)^2 1D shape rather than (dist x y)^2. * LipschitzSmoothWith.deriv_descent_le: descent inequality extractor. * LipschitzSmoothWith.deriv_sub_mul_le: variance bound on deriv. Gradient.lean: * lipschitzSmoothWith_iff_inner_gradient: characterisation on a Hilbert space in gradient form under Differentiable. * LipschitzSmoothWith.inner_gradient_descent_le: descent inequality extractor. * LipschitzSmoothWith.inner_gradient_sub_le: variance bound on the gradient. The descent lemma (converse direction), the LipschitzWith K (fderiv) <-> LipschitzWith K (gradient) Riesz isomorphism, and the Baillon-Haddad equivalence with cocoercivity under convexity remain deferred to follow-ups.
…bleAt The descent and variance-bound extractors at the FDeriv, Deriv, and Gradient layers previously required global Differentiable R f. Weaken to pointwise DifferentiableAt at the relevant point(s): * fderiv_descent_le, deriv_descent_le, inner_gradient_descent_le now take DifferentiableAt at x. * fderiv_apply_sub_le, fderiv_sub_apply_le, deriv_sub_mul_le, and inner_gradient_sub_le now take DifferentiableAt at both x and y. The iff lemmas (lipschitzSmoothWith_iff_fderiv, _deriv, _inner_gradient) keep Differentiable since they are global characterisations and genuinely require it.
Each theorem's docstring just restated the signature in English. The module-level 'Main results' lists already give a brief one-line description per declaration, which is sufficient. Per mathlib-design conventions, docstrings on theorems are encouraged only where they add information beyond the type signature. The def-level docstring on LipschitzSmoothWith itself is preserved.
* Basic.lean: add Deriv.lean to the sibling-file references in the file docstring. * Harmonise Main-results bullets across the four files: one-line descriptions with no embedded statement repetitions. * Gradient.lean: drop unused `open InnerProductSpace` — the file uses only inner-product-scoped notation (`open scoped RealInnerProductSpace`) and root-namespace lemmas like `inner_gradient_left`.
…ocstring * Replace the ▸ chain (lineDeriv_neg ▸ neg_sub ▸ dist_comm ▸) in the proof of lineDeriv_apply_sub_le with explicit `have` + `rw` + `linarith`. * Trim the module docstring from ~33 to ~22 lines: drop the per-sibling-file enumeration (the directory listing is self-evident) and remove repetition of the implementation-detail rationale.
Each file's ## Main results section listed the descent extractor and the two variance-bound packaging forms as separate bullets, which inflated the section without adding information. Consolidate to one bullet per file covering descent + variance-bound together, while keeping the iff lemma as a separate top-level entry.
Foo.{bar, baz} is Lean syntax for universe parameters and could confuse a
reader. Switch to mathlib-standard comma-separated qualified names.
* Drop `: Prop` annotation on `def LipschitzSmoothWith` (matches the `LipschitzWith` precedent in `Topology/EMetricSpace/Lipschitz.lean`). * Compact iff lemma signatures: put `LipschitzSmoothWith K f ↔` on the same line as the `theorem` keyword across all four files. * Inline single-line returns where the body is short (`lineDeriv_descent_le`, `fderiv_descent_le`, `deriv_descent_le`). * Rename `have hbase := ...` to `have := ...` (anonymous `this` binding) in `Deriv.lean` proofs.
Drop the per-file "Main results" / "Main definitions" enumerations from the four module docstrings; keep just the intro paragraph. The declarations bot already lists new declarations, and the file contents are short enough that the enumeration was pure duplication.
Introduce the `CocoerciveWith K f` predicate on a Hilbert space and the elementary direction `K`-cocoercive ⟹ `K`-Lipschitz gradient (Cauchy-Schwarz). The converse direction `K`-smooth + convex ⟹ `K`-cocoercive (Baillon-Haddad) is provided in a follow-up.
`CocoerciveWith` shares the Hilbert-space context with the gradient-form characterisations of `LipschitzSmoothWith` and was always going to be a small, focused file. Folding it eliminates one module with no import overhead — `Gradient.lean` already imports `Gradient.Basic`.
Change `LipschitzSmoothWith K f` from the one-sided descent inequality
f y ≤ f x + lineDeriv ℝ f x (y - x) + (K / 2) (dist x y)²
to the two-sided absolute-value form
|f y - f x - lineDeriv ℝ f x (y - x)| ≤ (K / 2) (dist x y)²
matching the textbook definition of L-smoothness (Lipschitz gradient,
class C^{1,1}) — orientation-agnostic, closed under f ↦ -f, and used in
Nesterov (Lemma 1.2.3), Beck (Ch. 5), Bauschke-Combettes (Lemma 2.64),
etc. The one-sided form admitted pathological cases like `-|x|` being
0-smooth, which the two-sided form excludes.
API changes:
- New primary extractor `lineDeriv_abs_le` (matching the def body).
- New lower-bound `lineDeriv_descent_ge` and two-sided variance
`lineDeriv_apply_sub_abs_le` extractors.
- `LipschitzSmoothWith.hasLineDerivAt` and `lineDifferentiableAt`:
the two-sided form unlocks line-differentiability everywhere,
provable from the predicate's bound
`|f(x + tv) - f x - t·L| ≤ K/2 t²‖v‖² = o(t)`.
- Existing extractors `lineDeriv_descent_le`, `lineDeriv_apply_sub_le`,
`lineDeriv_sub_apply_le` retained (one-sided, derived from the abs).
- Parallel additions in `FDeriv.lean`, `Deriv.lean`, `Gradient.lean`.
- `CocoerciveWith` and `CocoerciveWith.lipschitzWith_gradient` unchanged.
Fill in `LipschitzSmoothWith.hasLineDerivAt`: a `K`-smooth function is line-differentiable everywhere, and the `lineDeriv` value at every direction is the actual line derivative. The predicate bound |f(x + t·v) - f x - t · lineDeriv f x v| ≤ K/2 · t² · ‖v‖² (obtained by applying the abs-bound at `(x, x + t • v)` and factoring `t` via `lineDeriv_smul`) is `o(t)`, which is the `IsLittleO` form of `HasDerivAt` at `0` for the 1D restriction. The `continuous` field remains `sorry` pending a separate argument.
- rename lineMap_contDiff{,_uncurry} → contDiff_lineMap{,_uncurry}
- trim module docstring to first declaration
- demote new Poincare import to non-public
- inline `refine .congr ?_ this; fun_prop` as `exact .congr (by fun_prop) this`
Splits the existing `PathOperations` section into a dedicated `Segment` section with `[NormedSpace ℝ E]` hoisted to the variable block, and adds: - `curveIntegrable_segment_const` - `ContinuousOn.curveIntegrable_of_contDiffOn` - `Path.segment_contDiffOn` - `ContinuousOn.curveIntegrable_segment`, `Continuous.curveIntegrable_segment` - `curveIntegral_fderiv_segment` — FTC along a line segment `curveIntegrable_segment` is renamed to `curveIntegrable_segment_iff` (deprecated alias retained).
- Drop rename of `curveIntegrable_segment`: `curveIntegrable_segment_const` takes a different name slot, so deprecation is unnecessary - Restrict `curveIntegral_fderiv_segment` hypotheses to the segment (`DifferentiableAt` on the segment + `ContinuousOn` of the derivative) - Move `curveIntegral_fderiv_segment` from FDeriv section into Segment section, where the headline segment-FTC result belongs thematically - Make `a b` implicit in `Continuous.curveIntegrable_segment` for parity with the `ContinuousOn` variant - Keep `ContinuousOn.curveIntegrable_of_contDiffOn` at end of Segment section to reduce diff churn (it pre-existed in that position) - Drop docstrings that restate the type signature in English - Tag `Path.segment_contDiffOn` with `@[fun_prop]`
- demote AddTorsor.AffineMap and IntervalIntegral.FundThmCalculus to non-public imports (used only in proof bodies); restore IntervalIntegral.Basic as public since it provides IntervalIntegrable - rename Path.segment_contDiffOn → Path.contDiffOn_segment_extend per mathlib predicate-first naming convention (parallels the lineMap_contDiff → contDiff_lineMap rename in leanprover-community#39206)
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
The binrel elaborator inserts the NNReal-to-Real coercion at the leaf either way (verified: both spellings elaborate to the same term), so the explicit arrows were noise. Requested in review.
"extractor" is homemade terminology (review feedback); the upper/lower quadratic bounds are the standard descent lemma. Plain descriptive docstrings, no inline citations (not the mathlib per-theorem style).
Surnames without bib entries gesture at authority without giving the
reader anything to look up; the 'L-smoothness / C^{1,1}' framing already
signals it is the standard notion.
"variance" is a statistics term; these lemmas bound how much the line derivative changes (its variation) along y - x. Homemade wording, same category as the "extractor" fix.
Per review by j-loreaux on leanprover-community#39574, the predicate should not hard-code the codomain ℝ. `LipschitzSmoothWith K f` now takes `f : E → F` for any real normed space `F`, with the first-order Taylor remainder bound stated in norms: ‖f y - f x - lineDeriv ℝ f x (y - x)‖ ≤ K / 2 * (dist x y) ^ 2 All two-sided bounds generalize: the defining bound, the variation bound on the line derivative (now proved directly via the triangle inequality), `hasLineDerivAt`, and their fderiv forms; the 1D deriv form becomes `f : ℝ → F` via `fderiv_eq_smul_deriv`. The one-sided descent and variation bounds require an order on the codomain and stay specialized to real-valued `f` in dedicated `Real` sections; the Hilbert-space gradient file is unchanged apart from stating its two-sided bounds with ‖·‖ in place of |·|. Renames follow the naming convention (`abs` for |·|, `norm` for ‖·‖): `*_abs_le` → `*_norm_le`, `*_apply_sub_abs_le` → `*_apply_sub_norm_le`; no ℝ-specialized `abs` duplicates are kept (`Real.norm_eq_abs` is a simp lemma and rfl).
- replace have/rwa-at chains with simpa only ... using (Deriv, Gradient) - scalar section consumes the norm bounds directly by defeq (Real.norm_eq_abs is rfl): descent lemmas are one-line linarith, lineDeriv_apply_sub_le is term-mode le_of_abs_le - lineDeriv_apply_sub_norm_le: drop the calc block for norm_add_le + one abel rewrite + linarith
Adds first-order characterizations of convexity for differentiable functions: `f` is convex on `s` iff `f y ≥ f x + lineDeriv f x (y - x)` (and Fréchet / gradient analogues), plus the strict variant, the iff converse, and a few corollaries. * `Mathlib/Analysis/Convex/LineDeriv.lean` (new): the proof-content layer. `ConvexOn.lineRestriction`, `ConvexOn.add_lineDeriv_le`, `ConvexOn.lineDeriv_sub_apply_nonneg`, `ConcaveOn.le_add_lineDeriv`, `StrictConvexOn.add_lineDeriv_lt`, `convexOn_iff_add_lineDeriv_le`. * `Mathlib/Analysis/Convex/FDeriv.lean` (new): Fréchet-form lifts via `lineDeriv_eq_fderiv`. `ConvexOn.add_fderiv_le`, `ConvexOn.fderiv_sub_apply_nonneg`, `ConcaveOn.le_add_fderiv`, `StrictConvexOn.add_fderiv_lt`, `convexOn_iff_add_fderiv_le`. * `Mathlib/Analysis/Convex/Gradient.lean` (new): gradient-form lifts via Riesz (`inner_gradient_left`). `ConvexOn.add_inner_gradient_le`, `ConvexOn.inner_gradient_sub_nonneg`, `ConvexOn.isMinOn_of_gradient_eq_zero`, `ConcaveOn.le_add_inner_gradient`, `StrictConvexOn.add_inner_gradient_lt`, `convexOn_iff_add_inner_gradient_le`. * `Mathlib/Analysis/Convex/Deriv.lean` (additions): 1D additive form + line-restriction helper.
Must-fixes (1)–(3): - Add strict 1D additive forms `StrictConvexOn.add_hasDerivAt_mul_lt` and `StrictConcaveOn.lt_add_hasDerivAt_mul` (plus `deriv`-form variants) to `Convex/Deriv.lean`. - Refactor `StrictConvexOn.add_lineDeriv_lt` to use the new strict 1D additive form via `StrictConvexOn.lineRestriction` (drops the brittle midpoint `calc`). - Add `StrictConcaveOn.lt_add_lineDeriv`, `.lt_add_fderiv`, `.lt_add_inner_gradient` (missing concave strict duals across all three layers). - Add `ConvexOn.isMinOn_of_fderiv_eq_zero` (FDeriv-form sibling of the gradient one; needs only `NormedSpace ℝ E`, not Hilbert). - Add `HasLineDerivAt`- and `HasFDerivAt`-flavoured primitive forms for all inequality lemmas; the `lineDeriv` / `fderiv` versions become one-line corollaries via `LineDifferentiableAt.hasLineDerivAt` / `DifferentiableAt.hasFDerivAt`. Should-fixes (4)–(7): - Rename `_sub_apply_nonneg` → `_sub_nonneg` in both LineDeriv and FDeriv; `_apply` was vestigial for the scalar `lineDeriv` and added noise for `fderiv` where the application is visible in the statement. - Drop the LineDeriv-layer iff converse (`convexOn_iff_add_lineDeriv_le`); the FDeriv-layer iff is the canonical statement users want, and its premise `∀ x ∈ s, DifferentiableAt ℝ f x` is easier to instantiate than the pair-quantified line-differentiability of the dropped version. - Reprove `convexOn_iff_add_fderiv_le` directly using `fderiv`-arithmetic (no longer delegating through the dropped LineDeriv iff). - Rewrite Gradient module docstring to lead with "Hilbert space" framing. - Refactor the `▸` chain in `ConvexOn.lineDeriv_sub_nonneg` to a `have` + `rw` block. Bonus: factor out `private lineMap_eq_add_smul_sub` helper.
Concave duals and strict variants are systematic companions, not main results; fold them into one prose line per module docstring.
- replace have/rwa-at chains with simpa only ... using - drop a no-op change + simp only [smul_eq_mul] pair in convexOn_iff_add_fderiv_le (the calc closes the smul goal by defeq) - derive ConcaveOn.lineRestriction by neg-duality, matching the StrictConcaveOn version; factor the duplicated membership argument in StrictConvexOn.lineRestriction - simp_rw [inner_gradient_left] instead of a forall_congr'/imp_congr_right chain in convexOn_iff_add_inner_gradient_le
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.
PR summary d9e8bb5a9f
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.MeasureTheory.Integral.CurveIntegral.Basic | 2452 | 2468 | +16 (+0.65%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare |
5 |
Mathlib.MeasureTheory.Integral.CurveIntegral.Basic |
16 |
Mathlib.Analysis.Calculus.LipschitzSmooth.Basic (new file) |
1819 |
Mathlib.Analysis.Convex.LineDeriv (new file) |
1895 |
Mathlib.Analysis.Convex.FDeriv (new file) |
1896 |
Mathlib.Analysis.Convex.Gradient (new file) |
2269 |
Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv (new file) |
2540 |
Mathlib.Analysis.Calculus.LipschitzSmooth.Deriv (new file) |
2541 |
Mathlib.Analysis.Calculus.LipschitzSmooth.Gradient (new file) |
2545 |
Declarations diff (regex)
+ CocoerciveWith
+ CocoerciveWith.lipschitzWith_gradient
+ ConcaveOn.lineRestriction
+ Continuous.curveIntegrable_segment
+ ContinuousOn.curveIntegrable_segment
+ ConvexOn.lineRestriction
+ Differentiable.lipschitzSmoothWith_of_lipschitzWith
+ Differentiable.lipschitzSmoothWith_of_lipschitzWith_deriv
+ Differentiable.lipschitzSmoothWith_of_lipschitzWith_gradient
+ LipschitzSmoothOnSegmentWith
+ LipschitzSmoothOnSegmentWith.curveIntegral_norm_le
+ LipschitzSmoothOnSegmentWith.lipschitzSmoothWith
+ LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv
+ LipschitzSmoothWith
+ Path.contDiffOn_segment_extend
+ StrictConcaveOn.lineRestriction
+ StrictConvexOn.lineRestriction
+ add_deriv_mul_le
+ add_deriv_mul_lt
+ add_fderiv_le
+ add_fderiv_lt
+ add_hasDerivAt_mul_le
+ add_hasDerivAt_mul_lt
+ add_hasFDerivAt_le
+ add_hasFDerivAt_lt
+ add_hasLineDerivAt_le
+ add_hasLineDerivAt_lt
+ add_inner_gradient_le
+ add_inner_gradient_lt
+ add_lineDeriv_le
+ add_lineDeriv_lt
+ convexOn_iff_add_fderiv_le
+ convexOn_iff_add_inner_gradient_le
+ curveIntegrable_segment_const
+ curveIntegral_fderiv_segment
+ deriv_descent_ge
+ deriv_descent_le
+ deriv_norm_le
+ deriv_sub_mul_le
+ fderiv_apply_sub_le
+ fderiv_apply_sub_norm_le
+ fderiv_descent_ge
+ fderiv_descent_le
+ fderiv_norm_le
+ fderiv_sub_apply_le
+ fderiv_sub_nonneg
+ hasLineDerivAt
+ inner_gradient_descent_ge
+ inner_gradient_descent_le
+ inner_gradient_norm_le
+ inner_gradient_sub_le
+ inner_gradient_sub_nonneg
+ isMinOn_of_fderiv_eq_zero
+ isMinOn_of_gradient_eq_zero
+ le_add_deriv_mul
+ le_add_fderiv
+ le_add_hasDerivAt_mul
+ le_add_hasFDerivAt
+ le_add_hasLineDerivAt
+ le_add_inner_gradient
+ le_add_lineDeriv
+ lineDeriv_apply_sub_le
+ lineDeriv_apply_sub_norm_le
+ lineDeriv_descent_ge
+ lineDeriv_descent_le
+ lineDeriv_norm_le
+ lineDeriv_sub_apply_le
+ lineDeriv_sub_nonneg
+ lineDifferentiableAt
+ lineMap_eq_add_smul_sub
+ lipschitzSmoothWith_iff_deriv
+ lipschitzSmoothWith_iff_fderiv
+ lipschitzSmoothWith_iff_inner_gradient
+ lipschitzSmoothWith_iff_lineDeriv
+ lipschitzWith_fderiv_iff_lipschitzWith_deriv
+ lipschitzWith_fderiv_iff_lipschitzWith_gradient
+ lt_add_deriv_mul
+ lt_add_fderiv
+ lt_add_hasDerivAt_mul
+ lt_add_hasFDerivAt
+ lt_add_hasLineDerivAt
+ lt_add_inner_gradient
+ lt_add_lineDeriv
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
d9e8bb5).
- +82 new declarations
- −0 removed declarations
+CocoerciveWith
+CocoerciveWith.lipschitzWith_gradient
+ConcaveOn.le_add_deriv_mul
+ConcaveOn.le_add_fderiv
+ConcaveOn.le_add_hasDerivAt_mul
+ConcaveOn.le_add_hasFDerivAt
+ConcaveOn.le_add_hasLineDerivAt
+ConcaveOn.le_add_inner_gradient
+ConcaveOn.le_add_lineDeriv
+ConcaveOn.lineRestriction
+Continuous.curveIntegrable_segment
+ContinuousOn.curveIntegrable_segment
+ConvexOn.add_deriv_mul_le
+ConvexOn.add_fderiv_le
+ConvexOn.add_hasDerivAt_mul_le
+ConvexOn.add_hasFDerivAt_le
+ConvexOn.add_hasLineDerivAt_le
+ConvexOn.add_inner_gradient_le
+ConvexOn.add_lineDeriv_le
+ConvexOn.fderiv_sub_nonneg
+ConvexOn.inner_gradient_sub_nonneg
+ConvexOn.isMinOn_of_fderiv_eq_zero
+ConvexOn.isMinOn_of_gradient_eq_zero
+ConvexOn.lineDeriv_sub_nonneg
+ConvexOn.lineRestriction
+Differentiable.lipschitzSmoothWith_of_lipschitzWith
+Differentiable.lipschitzSmoothWith_of_lipschitzWith_deriv
+Differentiable.lipschitzSmoothWith_of_lipschitzWith_gradient
+LipschitzSmoothOnSegmentWith
+LipschitzSmoothOnSegmentWith.curveIntegral_norm_le
+LipschitzSmoothOnSegmentWith.lipschitzSmoothWith
+LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv
+LipschitzSmoothWith
+LipschitzSmoothWith.deriv_descent_ge
+LipschitzSmoothWith.deriv_descent_le
+LipschitzSmoothWith.deriv_norm_le
+LipschitzSmoothWith.deriv_sub_mul_le
+LipschitzSmoothWith.fderiv_apply_sub_le
+LipschitzSmoothWith.fderiv_apply_sub_norm_le
+LipschitzSmoothWith.fderiv_descent_ge
+LipschitzSmoothWith.fderiv_descent_le
+LipschitzSmoothWith.fderiv_norm_le
+LipschitzSmoothWith.fderiv_sub_apply_le
+LipschitzSmoothWith.hasLineDerivAt
+LipschitzSmoothWith.inner_gradient_descent_ge
+LipschitzSmoothWith.inner_gradient_descent_le
+LipschitzSmoothWith.inner_gradient_norm_le
+LipschitzSmoothWith.inner_gradient_sub_le
+LipschitzSmoothWith.lineDeriv_apply_sub_le
+LipschitzSmoothWith.lineDeriv_apply_sub_norm_le
+LipschitzSmoothWith.lineDeriv_descent_ge
+LipschitzSmoothWith.lineDeriv_descent_le
+LipschitzSmoothWith.lineDeriv_norm_le
+LipschitzSmoothWith.lineDeriv_sub_apply_le
+LipschitzSmoothWith.lineDifferentiableAt
+Path.contDiffOn_segment_extend
+StrictConcaveOn.lineRestriction
+StrictConcaveOn.lt_add_deriv_mul
+StrictConcaveOn.lt_add_fderiv
+StrictConcaveOn.lt_add_hasDerivAt_mul
+StrictConcaveOn.lt_add_hasFDerivAt
+StrictConcaveOn.lt_add_hasLineDerivAt
+StrictConcaveOn.lt_add_inner_gradient
+StrictConcaveOn.lt_add_lineDeriv
+StrictConvexOn.add_deriv_mul_lt
+StrictConvexOn.add_fderiv_lt
+StrictConvexOn.add_hasDerivAt_mul_lt
+StrictConvexOn.add_hasFDerivAt_lt
+StrictConvexOn.add_hasLineDerivAt_lt
+StrictConvexOn.add_inner_gradient_lt
+StrictConvexOn.add_lineDeriv_lt
+StrictConvexOn.lineRestriction
+convexOn_iff_add_fderiv_le
+convexOn_iff_add_inner_gradient_le
+curveIntegrable_segment_const
+curveIntegral_fderiv_segment
+lipschitzSmoothWith_iff_deriv
+lipschitzSmoothWith_iff_fderiv
+lipschitzSmoothWith_iff_inner_gradient
+lipschitzSmoothWith_iff_lineDeriv
+lipschitzWith_fderiv_iff_lipschitzWith_deriv
+lipschitzWith_fderiv_iff_lipschitzWith_gradientNo changes to strong technical debt.
No changes to weak technical debt.
Current commit d9e8bb5a9f
Reference commit 1c3e8f34a8
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
Bot
added
the
t-measure-probability
2 tasks
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
FordUniver
force-pushed
the
diffbase/lipschitzSmooth-convex
branch
from
99712f3 to
d9e8bb5
Compare
This was referenced Jul 8, 2026
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.
Establishes the descent lemma for
LipschitzSmoothWith: a differentiable functionf : E → Fbetween real normed spaces (Fcomplete) whose Fréchet derivative isK-Lipschitz isK-smooth. The 1Dderivand Hilbert-space gradient forms follow as corollaries. The proof routes through a segment-pointwise predicateLipschitzSmoothOnSegmentWithand the fundamental theorem of calculus along a line segment. Also adds the identification of Lipschitz constants between the Fréchet derivative and the gradient (via Riesz representation), and its 1Dderivanalogue.This is the substantive descent-lemma layer on top of the foundational
LipschitzSmoothWithpredicate API (#39574), whose codomain-generality it inherits. The Fréchet descent lemma proof uses segment-level curve integration (curveIntegral_fderiv_segment) fromMathlib.MeasureTheory.Integral.CurveIntegral. The gradient form usestoDual_comp_gradientto identifyfderiv ℝ fand∇ fas related by aLinearIsometryEquiv; the 1D analogue uses the isometry(ContinuousLinearMap.toSpanSingletonLIE ℝ ℝ).symm(evaluation at1) in the same way.LipschitzSmoothWithandCocoerciveWith#39574AffineMap.lineMap#39206inner_gradientlemmas #39203toDual_gradientand companions #39202Diff: link