From 4044022ca26063f4ea86f8ea4f53ef0e9f7e4ab4 Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 13:58:18 +0000 Subject: [PATCH] feat: strict convexity from an injective derivative, and steepness of the inverse of the derivative Co-Authored-By: Claude Code --- LMLExplore/Analysis/Convex/FDeriv.lean | 209 +++++++++++++++++++++++++ 1 file changed, 209 insertions(+) create mode 100644 LMLExplore/Analysis/Convex/FDeriv.lean diff --git a/LMLExplore/Analysis/Convex/FDeriv.lean b/LMLExplore/Analysis/Convex/FDeriv.lean new file mode 100644 index 0000000..d86104e --- /dev/null +++ b/LMLExplore/Analysis/Convex/FDeriv.lean @@ -0,0 +1,209 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +public import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps + +/-! +# Strict convexity and steepness through the derivative + +This file relates two properties of a convex function `f` to its derivative `f'`, in the form in +which they pass from a Legendre function to its conjugate. + +Strict convexity is injectivity of the derivative. A function with a subgradient at every point +of a convex set `s` is strictly convex on `s` as soon as no linear form is a subgradient at two +distinct points of `s`; conversely, a strictly convex function has no such common subgradient. +For a convex function with a derivative `f' x` at every point `x` of an open convex set `s`, the +subgradients are the derivatives, so `f` is strictly convex on `s` if and only if `f'` is +injective on `s`. The derivative of the conjugate of a Legendre function is the inverse of the +derivative of the function, which is injective, so this gives the strict convexity of the conjugate +[Roc70, Theorem 26.3]. + +Steepness passes to the inverse of the derivative. Let `f` be convex on an open set `s` of a proper +space (for instance a finite-dimensional one), with derivatives `f'` on `s` whose norm tends to +infinity at the frontier of `s`. Then for every linear form `b` that is not a derivative of `f` at a +point of `s`, the points of `s` whose derivative is close to `b` are far from the origin. In +particular, for every map `h` with `f' (h u) = u` and `h u ∈ s` for `u` in a set `t`, `‖h u‖` tends +to infinity as `u` tends to `b` within `t`. With `h` the derivative of the conjugate, this is the +steepness of the conjugate of a Legendre function [Roc70, Theorem 26.5; LS, Theorem 26.6]. + +## Main statements + +* `Convex.strictConvexOn_of_hasSubgradientWithinAt`: a function with a subgradient on `s` at every + point of `s` and no common subgradient at two distinct points is strictly convex on `s`. +* `StrictConvexOn.eq_of_hasSubgradientWithinAt`: two points of `s` at which a strictly convex + function has a common subgradient on `s` coincide. +* `StrictConvexOn.injOn_of_hasFDerivWithinAt`: the derivative of a strictly convex function is + injective. +* `ConvexOn.strictConvexOn_of_injOn`, `ConvexOn.strictConvexOn_iff_injOn`: a convex function with + derivatives on an open set is strictly convex there if and only if its derivative is injective. +* `ConvexOn.tendsto_norm_atTop_of_steep`: for a steep convex function and a linear form `b` that is + not a derivative at a point of `s`, `‖x‖ → ∞` as `x ∈ s` and `f' x → b`. +* `ConvexOn.tendsto_norm_comp_atTop_of_steep`: the same for a right inverse `h` of the derivative, + `‖h u‖ → ∞` as `u → b`. + +## References + +* [Roc70] R. T. Rockafellar, *Convex Analysis*, Princeton University Press, 1970, Section 26. +* [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020, + Section 26.4, Theorem 26.6. +-/ + +public section + +open Filter Set Topology + +variable {E : Type*} + +section Subgradient + +variable [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {s : Set E} {f : E → ℝ} + {g : E →L[ℝ] ℝ} {x y : E} + +/-- **Strict convexity from separated subgradients.** A function that has a subgradient on the +convex set `s` at every point of `s`, and no common subgradient at two distinct points of `s`, is +strictly convex on `s`. -/ +theorem Convex.strictConvexOn_of_hasSubgradientWithinAt (hs : Convex ℝ s) + (hsub : ∀ x ∈ s, ∃ g : E →L[ℝ] ℝ, HasSubgradientWithinAt f g s x) + (heq : ∀ x ∈ s, ∀ y ∈ s, ∀ g : E →L[ℝ] ℝ, + HasSubgradientWithinAt f g s x → HasSubgradientWithinAt f g s y → x = y) : + StrictConvexOn ℝ s f := by + refine ⟨hs, fun x hx y hy hxy a b ha hb hab ↦ ?_⟩ + -- A subgradient `g` at `z = a • x + b • y` is also one at `x` and `y` if `f` is affine on the + -- segment, which separation excludes. + obtain ⟨g, hg⟩ := hsub _ (hs hx hy ha.le hb.le hab) + set z := a • x + b • y + rw [hasSubgradientWithinAt_iff_le] at hg + have hgx := hg x hx + have hgy := hg y hy + have hv : a • (x - z) + b • (y - z) = 0 := by + rw [show a • (x - z) + b • (y - z) = z - (a + b) • z by simp only [z]; module, hab, one_smul, + sub_self] + have hlin : a * g (x - z) + b * g (y - z) = 0 := by + simpa only [map_add, map_smul, smul_eq_mul, map_zero] using congrArg g hv + simp only [smul_eq_mul] + by_contra hlt + push Not at hlt + -- `f` is affine on the segment: `g` touches `f` at `x` and at `y`. + have hz : (a + b) * f z = f z := by rw [hab, one_mul] + have hx_eq : f x = f z + g (x - z) := by + refine le_antisymm (not_lt.1 fun h ↦ ?_) hgx + nlinarith [mul_pos ha (sub_pos.2 h), mul_nonneg hb.le (sub_nonneg.2 hgy), hz] + have hy_eq : f y = f z + g (y - z) := by + refine le_antisymm (not_lt.1 fun h ↦ ?_) hgy + nlinarith [mul_pos hb (sub_pos.2 h), mul_nonneg ha.le (sub_nonneg.2 hgx), hz] + have htouch {w : E} (hw : f w = f z + g (w - z)) : HasSubgradientWithinAt f g s w := by + rw [hasSubgradientWithinAt_iff_le] + intro v hv + have : g (v - w) = g (v - z) - g (w - z) := by rw [← map_sub, sub_sub_sub_cancel_right] + linarith [hg v hv] + exact hxy (heq x hx y hy g (htouch hx_eq) (htouch hy_eq)) + +/-- **Strict convexity separates subgradients.** If `f` is strictly convex on `s` and `g` is a +subgradient of `f` on `s` at two points `x, y ∈ s`, then `x = y`. This is Tau Ceti's +`StrictConvexOn.eq_of_mem_subdifferential` for subgradients on a set. -/ +theorem StrictConvexOn.eq_of_hasSubgradientWithinAt (hf : StrictConvexOn ℝ s f) (hx : x ∈ s) + (hy : y ∈ s) (hgx : HasSubgradientWithinAt f g s x) (hgy : HasSubgradientWithinAt f g s y) : + x = y := by + have hmin {w : E} (hgw : HasSubgradientWithinAt f g s w) : + IsMinOn (f - ⇑g.toLinearMap) s w := by + rw [isMinOn_iff] + intro v hv + have := hasSubgradientWithinAt_iff_le.1 hgw v hv + simp only [Pi.sub_apply, ContinuousLinearMap.coe_coe, map_sub] at this ⊢ + linarith + exact (hf.sub_concaveOn (g.toLinearMap.concaveOn hf.1)).eq_of_isMinOn (hmin hgx) (hmin hgy) hx hy + +end Subgradient + +variable [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {f : E → ℝ} + {f' : E → E →L[ℝ] ℝ} + +/-- **The derivative of a strictly convex function is injective.** If `f` is strictly convex on +`s` with derivative `f' x` within `s` at every `x ∈ s`, then `f'` is injective on `s`. -/ +theorem StrictConvexOn.injOn_of_hasFDerivWithinAt (hf : StrictConvexOn ℝ s f) + (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) : s.InjOn f' := fun x hx y hy hxy ↦ + hf.eq_of_hasSubgradientWithinAt hx hy ((hf' x hx).hasSubgradientWithinAt hf.convexOn hx) + (hxy ▸ (hf' y hy).hasSubgradientWithinAt hf.convexOn hy) + +/-- **Strict convexity from an injective derivative.** A function convex on an open set `s`, with +derivative `f' x` at every `x ∈ s`, is strictly convex on `s` if `f'` is injective on `s`. -/ +theorem ConvexOn.strictConvexOn_of_injOn (hf : ConvexOn ℝ s f) (hs : IsOpen s) + (hf' : ∀ x ∈ s, HasFDerivAt f (f' x) x) (hinj : s.InjOn f') : StrictConvexOn ℝ s f := + hf.1.strictConvexOn_of_hasSubgradientWithinAt + (fun x hx ↦ ⟨f' x, (hf' x hx).hasSubgradientWithinAt hf hx⟩) + fun x hx y hy _ hgx hgy ↦ hinj hx hy <| + ((hf' x hx).eq_of_hasSubgradientWithinAt (hs.mem_nhds hx) hgx).symm.trans + ((hf' y hy).eq_of_hasSubgradientWithinAt (hs.mem_nhds hy) hgy) + +/-- A function convex on an open set `s`, with derivative `f' x` at every `x ∈ s`, is strictly +convex on `s` if and only if `f'` is injective on `s`. -/ +theorem ConvexOn.strictConvexOn_iff_injOn (hf : ConvexOn ℝ s f) (hs : IsOpen s) + (hf' : ∀ x ∈ s, HasFDerivAt f (f' x) x) : StrictConvexOn ℝ s f ↔ s.InjOn f' := + ⟨fun h ↦ h.injOn_of_hasFDerivWithinAt fun x hx ↦ (hf' x hx).hasFDerivWithinAt, + hf.strictConvexOn_of_injOn hs hf'⟩ + +/-- **Steepness passes to the inverse of the derivative.** Let `f` be convex on an open set `s` of +a proper space, with derivative `f' x` at every `x ∈ s`, and steep: `‖f' y‖ → ∞` as `y` tends +within `s` to a point of the frontier of `s`. If the linear form `b` is not the derivative of `f` +at a point of `s`, then `‖x‖ → ∞` as `x ∈ s` and `f' x → b`. -/ +theorem ConvexOn.tendsto_norm_atTop_of_steep [ProperSpace E] (hf : ConvexOn ℝ s f) + (hs : IsOpen s) (hf' : ∀ x ∈ s, HasFDerivAt f (f' x) x) + (hsteep : ∀ x ∈ frontier s, Tendsto (fun y ↦ ‖f' y‖) (𝓝[s] x) atTop) + {b : E →L[ℝ] ℝ} (hb : b ∉ f' '' s) : + Tendsto (fun x ↦ ‖x‖) (comap f' (𝓝 b) ⊓ 𝓟 s) atTop := by + -- A bounded family of such points has a cluster point `x` in the closure of `s`. If `x ∈ s`, the + -- subgradient inequalities at the nearby points pass to the limit and make `b` a subgradient, + -- hence the derivative, at `x`; if `x` is on the frontier, steepness contradicts `f' → b`. + rw [Filter.tendsto_atTop] + intro R + by_contra hR + rw [not_eventually, frequently_iff_neBot] at hR + have hball : 𝓟 {y : E | ¬R ≤ ‖y‖} ≤ 𝓟 (Metric.closedBall 0 R) := + principal_mono.2 fun y (hy : ¬R ≤ ‖y‖) ↦ by simpa using (not_le.1 hy).le + obtain ⟨x, -, hx⟩ := (isCompact_closedBall (0 : E) R).exists_clusterPt + (f := comap f' (𝓝 b) ⊓ 𝓟 s ⊓ 𝓟 {y | ¬R ≤ ‖y‖}) (inf_le_right.trans hball) + -- `H` is the filter of points of `s` near `x` with derivative near `b`. + set H := 𝓝 x ⊓ (comap f' (𝓝 b) ⊓ 𝓟 s ⊓ 𝓟 {y | ¬R ≤ ‖y‖}) + have : H.NeBot := hx + have hHx : H ≤ 𝓝 x := inf_le_left + have hHs : H ≤ 𝓟 s := inf_le_right.trans (inf_le_left.trans inf_le_right) + have hHb : Tendsto f' H (𝓝 b) := + tendsto_comap.mono_left (inf_le_right.trans (inf_le_left.trans inf_le_left)) + by_cases hxs : x ∈ s + · -- `b` is a subgradient of `f` on `s` at `x`, hence the derivative there. + refine hb ⟨x, hxs, ((hf' x hxs).eq_of_hasSubgradientWithinAt (hs.mem_nhds hxs) ?_).symm⟩ + rw [hasSubgradientWithinAt_iff_le] + intro y hy + have hlim : Tendsto (fun z ↦ f z + f' z (y - z)) H (𝓝 (f x + b (y - x))) := + (((hf' x hxs).continuousAt.tendsto.mono_left hHx)).add <| + (isBoundedBilinearMap_apply.continuous.tendsto (b, y - x)).comp <| + hHb.prodMk_nhds ((tendsto_const_nhds.sub tendsto_id).mono_left hHx) + refine le_of_tendsto hlim ?_ + filter_upwards [le_principal_iff.1 hHs] with z hz + exact hasSubgradientWithinAt_iff_le.1 ((hf' z hz).hasSubgradientWithinAt hf hz) y hy + · -- `x` is on the frontier of `s`, where steepness contradicts `f' → b`. + have hxcl : x ∈ closure s := + mem_closure_iff_clusterPt.2 (NeBot.mono this (le_inf hHx hHs)) + have hxf : x ∈ frontier s := by rw [hs.frontier_eq]; exact ⟨hxcl, hxs⟩ + exact not_tendsto_atTop_of_tendsto_nhds (hHb.norm) + ((hsteep x hxf).mono_left (le_inf hHx hHs)) + +/-- **Steepness passes to the inverse of the derivative**, for a right inverse. Under the +hypotheses of `ConvexOn.tendsto_norm_atTop_of_steep`, let `h` map a set `t` of linear forms into +`s` with `f' (h u) = u` for `u ∈ t`. Then `‖h u‖ → ∞` as `u` tends to `b` within `t`. -/ +theorem ConvexOn.tendsto_norm_comp_atTop_of_steep [ProperSpace E] (hf : ConvexOn ℝ s f) + (hs : IsOpen s) (hf' : ∀ x ∈ s, HasFDerivAt f (f' x) x) + (hsteep : ∀ x ∈ frontier s, Tendsto (fun y ↦ ‖f' y‖) (𝓝[s] x) atTop) + {b : E →L[ℝ] ℝ} (hb : b ∉ f' '' s) {t : Set (E →L[ℝ] ℝ)} {h : (E →L[ℝ] ℝ) → E} + (hmaps : MapsTo h t s) (hinv : ∀ u ∈ t, f' (h u) = u) : + Tendsto (fun u ↦ ‖h u‖) (𝓝[t] b) atTop := by + refine (hf.tendsto_norm_atTop_of_steep hs hf' hsteep hb).comp (tendsto_inf.2 ⟨?_, ?_⟩) + · rw [tendsto_comap_iff] + exact tendsto_nhdsWithin_congr (fun u hu ↦ (hinv u hu).symm) + (tendsto_id.mono_left nhdsWithin_le_nhds) + · exact tendsto_principal.2 (eventually_mem_nhdsWithin.mono fun u hu ↦ hmaps hu)