feat(Analysis/Calculus/LipschitzSmooth): add descent lemma#41495

Open

FordUniver wants to merge 43 commits into

leanprover-community:masterfrom

FordUniver:diffbase/lipschitzSmooth-convex

Commits on May 11, 2026

Commits on May 17, 2026

added simp attribute and additional lemma by Komyyy's suggestion
FordUniver
committed

Commits on May 18, 2026

Commits on May 20, 2026

Commits on Jul 8, 2026

Merge branch 'master' into feat/curveIntegral-segment-FTC
FordUniver
authored
Merge branch 'master' into feat/lipschitzSmooth-basic
FordUniver
authored
Update Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean

FordUniver
and
j-loreaux
authored
Update Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean

FordUniver
and
j-loreaux
authored
chore: drop redundant coercion arrows on K, fix sub_apply deprecation
FordUniver
committed
chore: replace "extractor" jargon with plain descriptions in docstrings
FordUniver
committed
chore: drop bare author name-drop from module docstring
FordUniver
committed
chore: "variance" -> "variation" in line-derivative bound docstrings
FordUniver
committed
feat: generalize LipschitzSmoothWith codomain to normed spaces
FordUniver
committed
style: tighten proofs after codomain generalization
FordUniver
committed
Merge remote-tracking branch 'origin/feat/curveIntegral-segment-FTC' into HEAD
FordUniver
committed
feat(Analysis/Convex): first-order convexity inequalities
FordUniver
committed
refactor(Analysis/Convex): apply review feedback
FordUniver
committed
chore(Analysis/Convex): trim main-results lists to the main statements
FordUniver
committed
refactor(Analysis/Convex): tighten proofs
FordUniver
committed
chore(Analysis/Convex): ContinuousLinearMap.sub_apply -> sub_apply (deprecation)
FordUniver
committed
feat(Analysis/Calculus/LipschitzSmooth): add descent lemma
FordUniver
committed
Merge remote-tracking branch 'origin/feat/convex-first-order-inequalities' into HEAD
FordUniver
committed