From bc5ae1ddc30d0097c4af30343e029d3e73ebf0c3 Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 15:45:17 +0000 Subject: [PATCH 1/3] feat: the conjugate of a Legendre function is Legendre [LS, Theorem 26.6] Prove that the derivative of a Legendre function is a bijection from the interior of its domain onto the interior of the domain of its conjugate, with inverse the derivative of the conjugate; Bregman duality in Legendre form; and that the conjugate is Legendre. Move Legendre.lean to Legendre/Basic.lean and let its existence of constrained minimizers start from a bounded sublevel set. Co-Authored-By: Claude Code --- LMLExplore/Analysis/Convex/Conjugate.lean | 22 +- .../{Legendre.lean => Legendre/Basic.lean} | 82 +++++--- .../Analysis/Convex/Legendre/Conjugate.lean | 188 ++++++++++++++++++ 3 files changed, 262 insertions(+), 30 deletions(-) rename LMLExplore/Analysis/Convex/{Legendre.lean => Legendre/Basic.lean} (89%) create mode 100644 LMLExplore/Analysis/Convex/Legendre/Conjugate.lean diff --git a/LMLExplore/Analysis/Convex/Conjugate.lean b/LMLExplore/Analysis/Convex/Conjugate.lean index 78c5dd7..2683673 100644 --- a/LMLExplore/Analysis/Convex/Conjugate.lean +++ b/LMLExplore/Analysis/Convex/Conjugate.lean @@ -8,6 +8,7 @@ module public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv public import LMLExplore.Analysis.Convex.Bregman.StrictConvex public import Mathlib.Analysis.Normed.Operator.Bilinear +public import TauCeti.Analysis.Convex.EffectiveDomain public import TauCeti.Analysis.Convex.Subdifferential /-! @@ -34,8 +35,9 @@ conjugate that hold at every subgradient of an interior point [LS, Theorem 26.6] neighbourhood of `u` and differentiable at `u` with derivative evaluation at `x`. For a differentiable `F` the subgradient is `∇F(x)`, so `∇F⋆ (∇F x) = x`: the gradient of the conjugate is a left inverse of the gradient of `F` on the interior of the domain, and `∇F` - maps that interior into the interior of the domain of `F⋆`. That `∇F` is onto the interior of - the domain of `F⋆`, the rest of [LS, Theorem 26.6 (a)], is not proved here. + maps that interior into the interior of the domain of `F⋆`. For a Legendre function `F`, the + rest of [LS, Theorem 26.6] (that `∇F` is onto the interior of the domain of `F⋆`, and that + `F⋆` is Legendre) is in `LMLExplore.Analysis.Convex.Legendre.Conjugate`. No lower semicontinuity of `F` at the boundary of `D` is needed, and `F` need not be differentiable. The differentiability of `F⋆` comes from a uniform growth bound: the Bregman @@ -50,6 +52,7 @@ divergence `z ↦ D_F(z, x)` grows linearly away from `x` * `LMLExplore.fenchelConjugateOn_eq_fenchelConjugate`: the conversion to Tau Ceti's `fenchelConjugate`. +* `LMLExplore.convexOn_toReal_fenchelConjugateOn`: the conjugate is convex on its effective domain. * `LMLExplore.hasSubgradientWithinAt_iff_fenchelConjugateOn_eq`: the Fenchel–Young equality. * `LMLExplore.bregDiv_toReal_fenchelConjugateOn`: `D_{F⋆}(v, u) = D_F(x, y)` [LS, Theorem 26.6 (b)]. * `LMLExplore.hasFDerivAt_toReal_fenchelConjugateOn`: the conjugate has derivative evaluation at `x` @@ -129,6 +132,21 @@ theorem fenchelConjugateOn_ne_bot (hx : x ∈ D) (u : E →L[ℝ] ℝ) : fenchelConjugateOn F D u ≠ ⊥ := ne_bot_of_le_ne_bot (by simp [← EReal.coe_sub]) (sub_le_fenchelConjugateOn hx u) +/-- The real representative of the conjugate on `D` is convex on the effective domain +`{u | F⋆ u ≠ ⊤}` of the conjugate. -/ +theorem convexOn_toReal_fenchelConjugateOn : + ConvexOn ℝ {u | fenchelConjugateOn F D u ≠ ⊤} fun u ↦ (fenchelConjugateOn F D u).toReal := by + classical + -- On the empty set the conjugate is `⊥`, whose real representative is `0`. + rcases D.eq_empty_or_nonempty with rfl | ⟨x, hx⟩ + · simpa [fenchelConjugateOn_eq_iSup] using convexOn_const (0 : ℝ) convex_univ + have heq : fenchelConjugateOn F D = TauCeti.fenchelConjugate (topDualPairing ℝ E).flip + (fun x ↦ if x ∈ D then (F x : EReal) else ⊤) := + funext (fenchelConjugateOn_eq_fenchelConjugate F D) + rw [heq] + exact TauCeti.convexOn_toReal (TauCeti.convex_epigraph_fenchelConjugate _ _) + fun u ↦ heq ▸ fenchelConjugateOn_ne_bot hx u + /-- **The Fenchel–Young inequality** on `D` for real representatives: `u x - F x ≤ F⋆ u` for `x ∈ D` when `F⋆ u` is finite. -/ theorem sub_le_toReal_fenchelConjugateOn (hx : x ∈ D) (hu : fenchelConjugateOn F D u ≠ ⊤) : diff --git a/LMLExplore/Analysis/Convex/Legendre.lean b/LMLExplore/Analysis/Convex/Legendre/Basic.lean similarity index 89% rename from LMLExplore/Analysis/Convex/Legendre.lean rename to LMLExplore/Analysis/Convex/Legendre/Basic.lean index 4641045..acd0e5b 100644 --- a/LMLExplore/Analysis/Convex/Legendre.lean +++ b/LMLExplore/Analysis/Convex/Legendre/Basic.lean @@ -56,6 +56,8 @@ differentiable. In finite dimension, if `F` has a minimizer `y₀` over `D`, then for every closed convex `A` meeting the interior of `D`, `F` has a unique minimizer over `A ∩ D`, and the minimizers of `F` over any set are those of the Bregman divergence `D_F(·, y₀)`. +* `IsLegendre.existsUnique_isMinOn_inter_of_isBounded`: the same existence and uniqueness when, + instead, some `x₀ ∈ A` interior to `D` has a bounded sublevel set `{x ∈ A ∩ D | F x ≤ F x₀}`. * `IsLegendre.bregDiv`: the Bregman divergence `D_F(·, y)` of a Legendre function is Legendre. * `IsLegendre.existsUnique_isMinOn_bregDiv`, `IsLegendre.mem_interior_of_isMinOn_bregDiv`: in @@ -360,25 +362,36 @@ private lemma apply_add_smul_sub_le_of_tendsto {x₀ b : E} {m : ℝ} {u : ℕ rwa [smul_eq_mul, smul_eq_mul, show (1 - α) • x₀ + α • u n = x₀ + α • (u n - x₀) by module] at this -/-- Existence in [LS, Theorem 26.15 (a)]: in finite dimension, a Legendre function with a -minimizer over its domain attains its minimum over `A ∩ D` for every closed convex `A` meeting the -interior of `D`. -/ +/-- Existence in [LS, Theorem 26.15 (a)]: in finite dimension, a Legendre function attains its +minimum over `A ∩ D`, for a closed convex `A`, as soon as some `x₀ ∈ A` interior to `D` has a +bounded sublevel set `{x ∈ A ∩ D | F x ≤ F x₀}`. -/ private lemma exists_isMinOn_inter [FiniteDimensional ℝ E] (hA : IsClosed A) (hAc : Convex ℝ A) - (hAD : (A ∩ interior D).Nonempty) {y₀ : E} (hy₀ : y₀ ∈ D) (hmin : IsMinOn F D y₀) : + {x₀ : E} (hx₀ : x₀ ∈ A ∩ interior D) (hbdd : Bornology.IsBounded {x ∈ A ∩ D | F x ≤ F x₀}) : ∃ y ∈ A ∩ D, IsMinOn F (A ∩ D) y := by - obtain ⟨x₀, hx₀A, hx₀⟩ := hAD - -- A minimizing sequence `u n`, bounded since it stays in a sublevel set. - have hbdd : BddBelow (F '' (A ∩ D)) := - ⟨F y₀, forall_mem_image.2 fun x hx ↦ isMinOn_iff.1 hmin x hx.2⟩ - obtain ⟨v, hv_anti, hv, hv_mem⟩ := exists_seq_tendsto_sInf (S := F '' (A ∩ D)) - ⟨F x₀, mem_image_of_mem F ⟨hx₀A, interior_subset hx₀⟩⟩ hbdd - set m := sInf (F '' (A ∩ D)) - have hm : ∀ y ∈ A ∩ D, m ≤ F y := fun y hy ↦ csInf_le hbdd (mem_image_of_mem F hy) + set S := {x ∈ A ∩ D | F x ≤ F x₀} + have hx₀S : x₀ ∈ S := ⟨⟨hx₀.1, interior_subset hx₀.2⟩, le_rfl⟩ + -- `F` is bounded below on the bounded set `S`, by the tangent inequality at `x₀`. + obtain ⟨R, hR⟩ := hbdd.subset_closedBall x₀ + have hbddS : BddBelow (F '' S) := by + refine ⟨F x₀ - ‖fderiv ℝ F x₀‖ * R, forall_mem_image.2 fun x hx ↦ ?_⟩ + have htan := hF.add_fderiv_apply_sub_le hx₀.2 hx.1.2 + have hL : |fderiv ℝ F x₀ (x - x₀)| ≤ ‖fderiv ℝ F x₀‖ * ‖x - x₀‖ := + (fderiv ℝ F x₀).le_opNorm (x - x₀) + have hxR : ‖fderiv ℝ F x₀‖ * ‖x - x₀‖ ≤ ‖fderiv ℝ F x₀‖ * R := + mul_le_mul_of_nonneg_left (by simpa [dist_eq_norm] using hR hx) (norm_nonneg _) + linarith [neg_abs_le (fderiv ℝ F x₀ (x - x₀))] + -- A minimizing sequence `u n` in the bounded set `S`, with values tending to `m = inf F`. + obtain ⟨v, -, hv, hv_mem⟩ := exists_seq_tendsto_sInf (S := F '' S) + ⟨F x₀, mem_image_of_mem F hx₀S⟩ hbddS + set m := sInf (F '' S) + have hm : ∀ y ∈ A ∩ D, m ≤ F y := fun y hy ↦ by + by_cases hyx : F y ≤ F x₀ + · exact csInf_le hbddS (mem_image_of_mem F ⟨hy, hyx⟩) + · exact (csInf_le hbddS (mem_image_of_mem F hx₀S)).trans (not_le.1 hyx).le choose u hu hFu using hv_mem - obtain ⟨b, hb, φ, hφ, hlim⟩ := tendsto_subseq_of_bounded (hF.isBounded_sublevel hy₀ hmin (v 0)) - fun n ↦ ⟨(hu n).2, (hFu n).le.trans (hv_anti (Nat.zero_le n))⟩ - have hbD : b ∈ closure D := closure_mono (sep_subset _ _) hb - have hbA : b ∈ A := hA.mem_of_tendsto hlim (Eventually.of_forall fun n ↦ (hu (φ n)).1) + obtain ⟨b, hb, φ, hφ, hlim⟩ := tendsto_subseq_of_bounded hbdd hu + have hbD : b ∈ closure D := closure_mono (fun x (hx : x ∈ S) ↦ hx.1.2) hb + have hbA : b ∈ A := hA.mem_of_tendsto hlim (Eventually.of_forall fun n ↦ (hu (φ n)).1.1) have hFlim : Tendsto (fun n ↦ F (u (φ n))) atTop (𝓝 m) := by simpa only [Function.comp_def, hFu] using hv.comp hφ.tendsto_atTop by_cases hbi : b ∈ interior D @@ -387,10 +400,28 @@ private lemma exists_isMinOn_inter [FiniteDimensional ℝ E] (hA : IsClosed A) ( tendsto_nhds_unique (((hF.hasFDerivAt hbi).continuousAt.tendsto).comp hlim) hFlim exact ⟨b, ⟨hbA, interior_subset hbi⟩, isMinOn_iff.2 fun y hy ↦ hFb ▸ hm y hy⟩ · -- A boundary limit point is impossible: `F < m` at some point of `A ∩ D`. - obtain ⟨α, hα, hlt⟩ := hF.exists_apply_add_smul_sub_lt hx₀ (hF.mem_frontier_interior hbD hbi) - fun α hα ↦ hF.apply_add_smul_sub_le_of_tendsto hx₀ hbD (fun n ↦ (hu (φ n)).2) hlim hFlim hα - exact absurd (hm _ ⟨hAc.add_smul_sub_mem hx₀A hbA ⟨hα.1.le, hα.2.le⟩, interior_subset - (hF.convex.add_smul_sub_mem_interior_of_mem_closure hx₀ hbD hα.1.le hα.2)⟩) (not_le.2 hlt) + obtain ⟨α, hα, hlt⟩ := hF.exists_apply_add_smul_sub_lt hx₀.2 + (hF.mem_frontier_interior hbD hbi) fun α hα ↦ hF.apply_add_smul_sub_le_of_tendsto hx₀.2 + hbD (fun n ↦ (hu (φ n)).1.2) hlim hFlim hα + exact absurd (hm _ ⟨hAc.add_smul_sub_mem hx₀.1 hbA ⟨hα.1.le, hα.2.le⟩, interior_subset + (hF.convex.add_smul_sub_mem_interior_of_mem_closure hx₀.2 hbD hα.1.le hα.2)⟩) + (not_le.2 hlt) + +/-- **Minimization of a Legendre function over a closed convex set**, from a bounded sublevel set. +In finite dimension, if `A` is closed and convex and some `x₀ ∈ A` interior to the domain `D` has a +bounded sublevel set `{x ∈ A ∩ D | F x ≤ F x₀}`, then `F` has a unique minimizer over `A ∩ D`. -/ +theorem existsUnique_isMinOn_inter_of_isBounded [FiniteDimensional ℝ E] (hA : IsClosed A) + (hAc : Convex ℝ A) {x₀ : E} (hx₀ : x₀ ∈ A ∩ interior D) + (hbdd : Bornology.IsBounded {x ∈ A ∩ D | F x ≤ F x₀}) : + ∃! y, y ∈ A ∩ D ∧ IsMinOn F (A ∩ D) y := by + obtain ⟨y, hy, hymin⟩ := hF.exists_isMinOn_inter hA hAc hx₀ hbdd + refine ⟨y, ⟨hy, hymin⟩, fun y' ⟨hy', hy'min⟩ ↦ ?_⟩ + -- Both minimizers are interior, where `F` is strictly convex. + have hi := hF.mem_interior_of_isMinOn_inter hAc ⟨x₀, hx₀⟩ hy hymin + have hi' := hF.mem_interior_of_isMinOn_inter hAc ⟨x₀, hx₀⟩ hy' hy'min + have hsub : A ∩ interior D ⊆ A ∩ D := inter_subset_inter_right A interior_subset + exact (hF.strictConvexOn.subset inter_subset_right (hAc.inter hF.convex.interior)).eq_of_isMinOn + (hy'min.of_subset hsub) (hymin.of_subset hsub) ⟨hy'.1, hi'⟩ ⟨hy.1, hi⟩ /-- **Minimization of a Legendre function over a closed convex set** [LS, Theorem 26.15 (a)]. In finite dimension, if `F` has a minimizer over its domain `D`, then for every closed convex set `A` @@ -398,14 +429,9 @@ meeting the interior of `D`, `F` has a unique minimizer over `A ∩ D`. -/ theorem existsUnique_isMinOn_inter [FiniteDimensional ℝ E] (hA : IsClosed A) (hAc : Convex ℝ A) (hAD : (A ∩ interior D).Nonempty) {y₀ : E} (hy₀ : y₀ ∈ D) (hmin : IsMinOn F D y₀) : ∃! y, y ∈ A ∩ D ∧ IsMinOn F (A ∩ D) y := by - obtain ⟨y, hy, hymin⟩ := hF.exists_isMinOn_inter hA hAc hAD hy₀ hmin - refine ⟨y, ⟨hy, hymin⟩, fun y' ⟨hy', hy'min⟩ ↦ ?_⟩ - -- Both minimizers are interior, where `F` is strictly convex. - have hi := hF.mem_interior_of_isMinOn_inter hAc hAD hy hymin - have hi' := hF.mem_interior_of_isMinOn_inter hAc hAD hy' hy'min - have hsub : A ∩ interior D ⊆ A ∩ D := inter_subset_inter_right A interior_subset - exact (hF.strictConvexOn.subset inter_subset_right (hAc.inter hF.convex.interior)).eq_of_isMinOn - (hy'min.of_subset hsub) (hymin.of_subset hsub) ⟨hy'.1, hi'⟩ ⟨hy.1, hi⟩ + obtain ⟨x₀, hx₀⟩ := hAD + exact hF.existsUnique_isMinOn_inter_of_isBounded hA hAc hx₀ + ((hF.isBounded_sublevel hy₀ hmin (F x₀)).subset fun x hx ↦ ⟨hx.1.2, hx.2⟩) /-- **The constrained minimizer is a Bregman projection** [LS, Theorem 26.15 (b)]. If `y₀` minimizes `F` over its domain, then on every set `S`, the minimizers of the Bregman divergence diff --git a/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean b/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean new file mode 100644 index 0000000..605e66b --- /dev/null +++ b/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean @@ -0,0 +1,188 @@ +/- +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 LMLExplore.Analysis.Convex.Coercive +public import LMLExplore.Analysis.Convex.Conjugate +public import LMLExplore.Analysis.Convex.FDeriv +public import LMLExplore.Analysis.Convex.Legendre.Basic +public import Mathlib.Analysis.Normed.Module.DoubleDual + +/-! +# The conjugate of a Legendre function + +Let `F` be a Legendre function with domain `D` in a finite-dimensional real normed space `E`, and +let `F⋆ = fenchelConjugateOn F D` be its conjugate on the dual `E →L[ℝ] ℝ`, with effective domain +`D⋆ = {u | F⋆ u ≠ ⊤}`. This file proves the duality theorem for Legendre functions +[LS, Theorem 26.6]: + +* the derivative `∇F` is a bijection from the interior of `D` onto the interior of `D⋆`, whose + inverse is the derivative of `F⋆`: `∇F⋆ (∇F x) = x`, where a point `x` of `E` is identified + with the evaluation `u ↦ u x` in the bidual; +* the Bregman divergences are dual: `D_F(x, y) = D_{F⋆}(∇F y, ∇F x)`; +* the real representative of `F⋆` is a Legendre function with domain `D⋆`. + +No lower semicontinuity of `F` at the boundary of `D` is assumed. The point of the interior of +`D` where `∇F = u`, for `u` interior to `D⋆`, is the minimizer of the tilted function `F - u` +over `D`, which exists because the sublevel sets of `F - u` are bounded +(`LMLExplore.isBounded_setOf_le_of_mem_interior_setOf_fenchelConjugate_ne_top`). This is the map +`∇F⋆` that mirror descent and follow the regularized leader with a Legendre potential use to +return from the dual to the interior of the domain. + +## Main statements + +* `LMLExplore.IsLegendre.bijOn_fderiv`: [LS, Theorem 26.6 (a)], `∇F` is a bijection from the + interior of `D` onto the interior of `D⋆`. +* `LMLExplore.IsLegendre.fderiv_toReal_fenchelConjugateOn_fderiv`, + `LMLExplore.IsLegendre.fderiv_toReal_fenchelConjugateOn_eq_apply_iff`: its inverse is `∇F⋆`. +* `LMLExplore.IsLegendre.bregDiv_toReal_fenchelConjugateOn`: [LS, Theorem 26.6 (b)], + `D_{F⋆}(∇F y, ∇F x) = D_F(x, y)`. +* `LMLExplore.IsLegendre.toReal_fenchelConjugateOn`: [LS, Theorem 26.6 (c)], `F⋆` is Legendre. + +## References + +* T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020, + Section 26.5, Theorem 26.6 [LS]. +* R. T. Rockafellar, *Convex Analysis*, Princeton University Press, 1970, Theorem 26.5. +-/ + +public section + +open Set Filter Topology + +namespace LMLExplore.IsLegendre + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : E → ℝ} {D : Set E} {x y : E} + {u : E →L[ℝ] ℝ} + +variable (hF : IsLegendre F D) +include hF + +/-- The derivative of a Legendre function is injective on the interior of its domain. -/ +theorem injOn_fderiv : (interior D).InjOn (fderiv ℝ F) := + hF.strictConvexOn.injOn_of_hasFDerivWithinAt fun _ hx ↦ (hF.hasFDerivAt hx).hasFDerivWithinAt + +variable [FiniteDimensional ℝ E] + +/-- The derivative of a Legendre function maps the interior of its domain into the interior of +the effective domain of its conjugate. -/ +theorem mapsTo_fderiv : + MapsTo (fderiv ℝ F) (interior D) (interior {u | fenchelConjugateOn F D u ≠ ⊤}) := + fun _ hx ↦ mem_interior_setOf_fenchelConjugateOn_ne_top hF.convexOn hF.strictConvexOn hx + (hF.hasSubgradientWithinAt hx) + +/-- **The derivative of a Legendre function is onto the interior of the domain of its +conjugate** (part of [LS, Theorem 26.6 (a)]). Every `u` in the interior of `{u | F⋆ u ≠ ⊤}` is +the derivative of `F` at a point of the interior of `D`. -/ +theorem surjOn_fderiv : + SurjOn (fderiv ℝ F) (interior D) (interior {u | fenchelConjugateOn F D u ≠ ⊤}) := by + classical + intro u hu + -- The tilted function `G = F - u` is Legendre, with bounded sublevel sets since `u` is interior + -- to the domain of the conjugate. + have hG := hF.add_linear (-u) + obtain ⟨x₀, hx₀⟩ := hF.nonempty_interior + simp only [fenchelConjugateOn_eq_fenchelConjugate] at hu + have hbdd : Bornology.IsBounded + {x ∈ univ ∩ D | F x + (-u) x ≤ F x₀ + (-u) x₀} := by + refine (isBounded_setOf_le_of_mem_interior_setOf_fenchelConjugate_ne_top hu + (F x₀ - u x₀)).subset fun x ⟨⟨_, hxD⟩, hx⟩ ↦ ?_ + simp only [neg_apply] at hx + simp only [mem_ofPred_eq, hxD, ↓reduceIte, EReal.coe_le_coe_iff] + linarith + -- Its minimizer `y` over `D` is interior, and `∇F y - u = 0` there. + obtain ⟨y, ⟨-, hyD⟩, hymin⟩ := (hG.existsUnique_isMinOn_inter_of_isBounded isClosed_univ + convex_univ ⟨mem_univ x₀, hx₀⟩ hbdd).exists + rw [univ_inter] at hymin + have hy := hG.mem_interior_of_isMinOn hyD hymin + refine ⟨y, hy, ?_⟩ + have h0 := hG.fderiv_eq_zero_of_isMinOn hyD hymin + rwa [fderiv_fun_add (hF.hasFDerivAt hy).differentiableAt (-u).differentiableAt, + ContinuousLinearMap.fderiv, add_neg_eq_zero] at h0 + +/-- **The derivative of a Legendre function is a bijection between interiors** +[LS, Theorem 26.6 (a)]: it maps the interior of the domain `D` bijectively onto the interior of +the effective domain `{u | F⋆ u ≠ ⊤}` of the conjugate. Its inverse is the derivative of the +conjugate (`fderiv_toReal_fenchelConjugateOn_fderiv`). -/ +theorem bijOn_fderiv : + BijOn (fderiv ℝ F) (interior D) (interior {u | fenchelConjugateOn F D u ≠ ⊤}) := + ⟨hF.mapsTo_fderiv, hF.injOn_fderiv, hF.surjOn_fderiv⟩ + +/-- **The derivative of the conjugate inverts the derivative** (part of +[LS, Theorem 26.6 (a)]): `∇F⋆ (∇F x) = x` for `x` in the interior of the domain, where `x` is +identified with the evaluation `u ↦ u x`. -/ +theorem fderiv_toReal_fenchelConjugateOn_fderiv (hx : x ∈ interior D) : + fderiv ℝ (fun u ↦ (fenchelConjugateOn F D u).toReal) (fderiv ℝ F x) = + ContinuousLinearMap.apply ℝ ℝ x := + (hasFDerivAt_toReal_fenchelConjugateOn hF.convexOn hF.strictConvexOn hx + (hF.hasSubgradientWithinAt hx)).fderiv + +/-- **The derivative of the conjugate is the inverse of the derivative** (part of +[LS, Theorem 26.6 (a)]): for `u` in the interior of the domain of the conjugate and `x` in the +interior of `D`, `∇F⋆ u = x` if and only if `∇F x = u`. -/ +theorem fderiv_toReal_fenchelConjugateOn_eq_apply_iff + (hu : u ∈ interior {u | fenchelConjugateOn F D u ≠ ⊤}) (hx : x ∈ interior D) : + fderiv ℝ (fun u ↦ (fenchelConjugateOn F D u).toReal) u = ContinuousLinearMap.apply ℝ ℝ x ↔ + fderiv ℝ F x = u := by + refine ⟨fun h ↦ ?_, fun h ↦ h ▸ hF.fderiv_toReal_fenchelConjugateOn_fderiv hx⟩ + obtain ⟨y, hy, rfl⟩ := hF.surjOn_fderiv hu + rw [hF.fderiv_toReal_fenchelConjugateOn_fderiv hy] at h + have hyx : y = x := SeparatingDual.eq_iff_forall_dual_eq (R := ℝ).2 fun g ↦ by + simpa using congr($h g) + rw [hyx] + +/-- **Duality of Bregman divergences for Legendre functions** [LS, Theorem 26.6 (b)]: for `x, y` +in the interior of the domain, `D_{F⋆}(∇F y, ∇F x) = D_F(x, y)`, where the divergence of the +conjugate is taken with its derivative at `∇F x`. -/ +theorem bregDiv_toReal_fenchelConjugateOn (hx : x ∈ interior D) (hy : y ∈ interior D) : + bregDiv (fun u ↦ (fenchelConjugateOn F D u).toReal) (fderiv ℝ F y) (fderiv ℝ F x) + (fderiv ℝ (fun u ↦ (fenchelConjugateOn F D u).toReal) (fderiv ℝ F x)) = + bregDiv F x y (fderiv ℝ F y) := by + rw [hF.fderiv_toReal_fenchelConjugateOn_fderiv hx] + exact LMLExplore.bregDiv_toReal_fenchelConjugateOn (hF.hasSubgradientWithinAt hx) + (hF.hasSubgradientWithinAt hy) (interior_subset hx) (interior_subset hy) + +/-- **The conjugate of a Legendre function is Legendre** [LS, Theorem 26.6 (c)]. In finite +dimension, the real representative of the conjugate `F⋆` is a Legendre function with domain the +effective domain `{u | F⋆ u ≠ ⊤}` of the conjugate. -/ +theorem toReal_fenchelConjugateOn : + IsLegendre (fun u ↦ (fenchelConjugateOn F D u).toReal) {u | fenchelConjugateOn F D u ≠ ⊤} := by + set D' := {u | fenchelConjugateOn F D u ≠ ⊤} + -- `g` inverts `∇F` on the interior of `D'`, and `∇F⋆ u` is the evaluation at `g u`. + set g := Function.invFunOn (fderiv ℝ F) (interior D) + have hmaps : MapsTo g (interior D') (interior D) := hF.surjOn_fderiv.mapsTo_invFunOn + have hinv : ∀ u ∈ interior D', fderiv ℝ F (g u) = u := hF.surjOn_fderiv.rightInvOn_invFunOn + have hderiv (u : E →L[ℝ] ℝ) (hu : u ∈ interior D') : + HasFDerivAt (fun u ↦ (fenchelConjugateOn F D u).toReal) + (ContinuousLinearMap.apply ℝ ℝ (g u)) u := by + have := hasFDerivAt_toReal_fenchelConjugateOn hF.convexOn hF.strictConvexOn (hmaps hu) + (hF.hasSubgradientWithinAt (hmaps hu)) + rwa [hinv u hu] at this + obtain ⟨x₀, hx₀⟩ := hF.nonempty_interior + have hconv : ConvexOn ℝ D' fun u ↦ (fenchelConjugateOn F D u).toReal := + convexOn_toReal_fenchelConjugateOn + refine ⟨hconv, ⟨_, hF.mapsTo_fderiv hx₀⟩, + fun u hu ↦ (hderiv u hu).differentiableAt.differentiableWithinAt, ?_, fun b hb ↦ ?_⟩ + · -- Strict convexity: the derivative `u ↦ g u` is injective. + refine (hconv.subset interior_subset hconv.1.interior).strictConvexOn_of_injOn + isOpen_interior hderiv fun u hu v hv h ↦ ?_ + have huv : g u = g v := SeparatingDual.eq_iff_forall_dual_eq (R := ℝ).2 fun f ↦ by + simpa using congr($h f) + rw [← hinv u hu, ← hinv v hv, huv] + · -- Steepness: `‖g u‖ → ∞` as `u` tends to a boundary point `b` of the interior of `D'`, which + -- is not a derivative of `F` on the interior of `D`. + have hb' : b ∉ fderiv ℝ F '' interior D := by + rw [hF.bijOn_fderiv.image_eq] + exact fun h ↦ hb.2 (by rwa [interior_interior]) + refine tendsto_atTop_mono' _ ?_ + ((hF.convexOn.subset interior_subset hF.convex.interior).tendsto_norm_comp_atTop_of_steep + isOpen_interior (fun _ hx ↦ hF.hasFDerivAt hx) hF.tendsto_norm_fderiv hb' hmaps hinv) + filter_upwards [self_mem_nhdsWithin] with u hu + rw [(hderiv u hu).fderiv] + exact NormedSpace.norm_le_dual_bound ℝ (g u) (norm_nonneg _) fun f ↦ by + simpa using (ContinuousLinearMap.apply ℝ ℝ (g u)).le_opNorm f + +end LMLExplore.IsLegendre From 530712484816e077642e74ce3667a479bd84456c Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 16:05:45 +0000 Subject: [PATCH 2/3] refactor: share the bidual-embedding facts in the Legendre conjugate proofs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Use NormedSpace.inclusionInDoubleDualLi for the injectivity and norm preservation of x ↦ ContinuousLinearMap.apply ℝ ℝ x, and point the Bregman projection docstring at the moved Legendre.Basic module. Co-Authored-By: Claude Code --- .../Analysis/Convex/Bregman/Projection.lean | 2 +- .../Analysis/Convex/Legendre/Conjugate.lean | 22 +++++++++++-------- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/LMLExplore/Analysis/Convex/Bregman/Projection.lean b/LMLExplore/Analysis/Convex/Bregman/Projection.lean index 9d4e48d..3cd4c27 100644 --- a/LMLExplore/Analysis/Convex/Bregman/Projection.lean +++ b/LMLExplore/Analysis/Convex/Bregman/Projection.lean @@ -26,7 +26,7 @@ For a Bregman projection this is the **generalized Pythagorean inequality** differentiable within `K` at `z`, then `D_F(x, z) + D_F(z, y) ≤ D_F(x, y)` for every `x ∈ K`. Neither the convexity of `F` nor a derivative of `F` at `y` is needed: `J` is any linear map. The existence, uniqueness and interiority of Bregman projections for Legendre functions are in -`LMLExplore.Analysis.Convex.Legendre`. +`LMLExplore.Analysis.Convex.Legendre.Basic`. ## Main statements diff --git a/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean b/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean index 605e66b..9b81248 100644 --- a/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean +++ b/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean @@ -58,6 +58,16 @@ namespace LMLExplore.IsLegendre variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : E → ℝ} {D : Set E} {x y : E} {u : E →L[ℝ] ℝ} +/-- The evaluation `x ↦ (u ↦ u x)` into the bidual is injective: it is +`NormedSpace.inclusionInDoubleDual`, by definition. -/ +private theorem apply_injective : + Function.Injective (ContinuousLinearMap.apply ℝ ℝ : E → (E →L[ℝ] ℝ) →L[ℝ] ℝ) := + (NormedSpace.inclusionInDoubleDualLi ℝ).injective + +/-- The evaluation `x ↦ (u ↦ u x)` into the bidual preserves the norm. -/ +private theorem norm_apply (x : E) : ‖ContinuousLinearMap.apply ℝ ℝ x‖ = ‖x‖ := + (NormedSpace.inclusionInDoubleDualLi ℝ).norm_map x + variable (hF : IsLegendre F D) include hF @@ -130,9 +140,7 @@ theorem fderiv_toReal_fenchelConjugateOn_eq_apply_iff refine ⟨fun h ↦ ?_, fun h ↦ h ▸ hF.fderiv_toReal_fenchelConjugateOn_fderiv hx⟩ obtain ⟨y, hy, rfl⟩ := hF.surjOn_fderiv hu rw [hF.fderiv_toReal_fenchelConjugateOn_fderiv hy] at h - have hyx : y = x := SeparatingDual.eq_iff_forall_dual_eq (R := ℝ).2 fun g ↦ by - simpa using congr($h g) - rw [hyx] + rw [apply_injective h] /-- **Duality of Bregman divergences for Legendre functions** [LS, Theorem 26.6 (b)]: for `x, y` in the interior of the domain, `D_{F⋆}(∇F y, ∇F x) = D_F(x, y)`, where the divergence of the @@ -169,9 +177,7 @@ theorem toReal_fenchelConjugateOn : · -- Strict convexity: the derivative `u ↦ g u` is injective. refine (hconv.subset interior_subset hconv.1.interior).strictConvexOn_of_injOn isOpen_interior hderiv fun u hu v hv h ↦ ?_ - have huv : g u = g v := SeparatingDual.eq_iff_forall_dual_eq (R := ℝ).2 fun f ↦ by - simpa using congr($h f) - rw [← hinv u hu, ← hinv v hv, huv] + rw [← hinv u hu, ← hinv v hv, apply_injective h] · -- Steepness: `‖g u‖ → ∞` as `u` tends to a boundary point `b` of the interior of `D'`, which -- is not a derivative of `F` on the interior of `D`. have hb' : b ∉ fderiv ℝ F '' interior D := by @@ -181,8 +187,6 @@ theorem toReal_fenchelConjugateOn : ((hF.convexOn.subset interior_subset hF.convex.interior).tendsto_norm_comp_atTop_of_steep isOpen_interior (fun _ hx ↦ hF.hasFDerivAt hx) hF.tendsto_norm_fderiv hb' hmaps hinv) filter_upwards [self_mem_nhdsWithin] with u hu - rw [(hderiv u hu).fderiv] - exact NormedSpace.norm_le_dual_bound ℝ (g u) (norm_nonneg _) fun f ↦ by - simpa using (ContinuousLinearMap.apply ℝ ℝ (g u)).le_opNorm f + rw [(hderiv u hu).fderiv, norm_apply] end LMLExplore.IsLegendre From 3653de4de43018b4ff02decee392cd8415245980 Mon Sep 17 00:00:00 2001 From: prevostad Date: Fri, 13 Nov 2026 16:23:22 +0000 Subject: [PATCH 3/3] refactor: make the bidual-embedding facts public in a general file MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move the injectivity and norm preservation of the evaluation map `ContinuousLinearMap.apply 𝕜 𝕜` into the bidual out of the private `LMLExplore.IsLegendre` helpers into the new general module `LMLExplore.Analysis.Normed.Module.DoubleDual`, as public `ContinuousLinearMap.apply_injective` and `ContinuousLinearMap.norm_apply_apply`, stated over any `RCLike` field. Co-Authored-By: Claude Code --- .../Analysis/Convex/Legendre/Conjugate.lean | 18 ++------ .../Analysis/Normed/Module/DoubleDual.lean | 44 +++++++++++++++++++ 2 files changed, 48 insertions(+), 14 deletions(-) create mode 100644 LMLExplore/Analysis/Normed/Module/DoubleDual.lean diff --git a/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean b/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean index 9b81248..9a5109a 100644 --- a/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean +++ b/LMLExplore/Analysis/Convex/Legendre/Conjugate.lean @@ -9,7 +9,7 @@ public import LMLExplore.Analysis.Convex.Coercive public import LMLExplore.Analysis.Convex.Conjugate public import LMLExplore.Analysis.Convex.FDeriv public import LMLExplore.Analysis.Convex.Legendre.Basic -public import Mathlib.Analysis.Normed.Module.DoubleDual +public import LMLExplore.Analysis.Normed.Module.DoubleDual /-! # The conjugate of a Legendre function @@ -58,16 +58,6 @@ namespace LMLExplore.IsLegendre variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : E → ℝ} {D : Set E} {x y : E} {u : E →L[ℝ] ℝ} -/-- The evaluation `x ↦ (u ↦ u x)` into the bidual is injective: it is -`NormedSpace.inclusionInDoubleDual`, by definition. -/ -private theorem apply_injective : - Function.Injective (ContinuousLinearMap.apply ℝ ℝ : E → (E →L[ℝ] ℝ) →L[ℝ] ℝ) := - (NormedSpace.inclusionInDoubleDualLi ℝ).injective - -/-- The evaluation `x ↦ (u ↦ u x)` into the bidual preserves the norm. -/ -private theorem norm_apply (x : E) : ‖ContinuousLinearMap.apply ℝ ℝ x‖ = ‖x‖ := - (NormedSpace.inclusionInDoubleDualLi ℝ).norm_map x - variable (hF : IsLegendre F D) include hF @@ -140,7 +130,7 @@ theorem fderiv_toReal_fenchelConjugateOn_eq_apply_iff refine ⟨fun h ↦ ?_, fun h ↦ h ▸ hF.fderiv_toReal_fenchelConjugateOn_fderiv hx⟩ obtain ⟨y, hy, rfl⟩ := hF.surjOn_fderiv hu rw [hF.fderiv_toReal_fenchelConjugateOn_fderiv hy] at h - rw [apply_injective h] + rw [ContinuousLinearMap.apply_injective h] /-- **Duality of Bregman divergences for Legendre functions** [LS, Theorem 26.6 (b)]: for `x, y` in the interior of the domain, `D_{F⋆}(∇F y, ∇F x) = D_F(x, y)`, where the divergence of the @@ -177,7 +167,7 @@ theorem toReal_fenchelConjugateOn : · -- Strict convexity: the derivative `u ↦ g u` is injective. refine (hconv.subset interior_subset hconv.1.interior).strictConvexOn_of_injOn isOpen_interior hderiv fun u hu v hv h ↦ ?_ - rw [← hinv u hu, ← hinv v hv, apply_injective h] + rw [← hinv u hu, ← hinv v hv, ContinuousLinearMap.apply_injective h] · -- Steepness: `‖g u‖ → ∞` as `u` tends to a boundary point `b` of the interior of `D'`, which -- is not a derivative of `F` on the interior of `D`. have hb' : b ∉ fderiv ℝ F '' interior D := by @@ -187,6 +177,6 @@ theorem toReal_fenchelConjugateOn : ((hF.convexOn.subset interior_subset hF.convex.interior).tendsto_norm_comp_atTop_of_steep isOpen_interior (fun _ hx ↦ hF.hasFDerivAt hx) hF.tendsto_norm_fderiv hb' hmaps hinv) filter_upwards [self_mem_nhdsWithin] with u hu - rw [(hderiv u hu).fderiv, norm_apply] + rw [(hderiv u hu).fderiv, ContinuousLinearMap.norm_apply_apply] end LMLExplore.IsLegendre diff --git a/LMLExplore/Analysis/Normed/Module/DoubleDual.lean b/LMLExplore/Analysis/Normed/Module/DoubleDual.lean new file mode 100644 index 0000000..7734067 --- /dev/null +++ b/LMLExplore/Analysis/Normed/Module/DoubleDual.lean @@ -0,0 +1,44 @@ +/- +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 Mathlib.Analysis.Normed.Module.DoubleDual + +/-! +# The evaluation map into the bidual + +For a normed space `E` over `𝕜 = ℝ` or `ℂ`, the evaluation map +`ContinuousLinearMap.apply 𝕜 𝕜 : E →L[𝕜] (E →L[𝕜] 𝕜) →L[𝕜] 𝕜`, `x ↦ (u ↦ u x)`, is by +definition the inclusion `NormedSpace.inclusionInDoubleDual 𝕜 E` of `E` into its bidual. This file +states, in terms of `ContinuousLinearMap.apply`, that it is an isometry, so injective. These are +the forms used by statements that identify a point `x` with the evaluation at `x`, such as the +derivative of a Fenchel conjugate. + +## Main statements + +* `ContinuousLinearMap.norm_apply_apply`: `‖ContinuousLinearMap.apply 𝕜 𝕜 x‖ = ‖x‖`. +* `ContinuousLinearMap.apply_injective`: `ContinuousLinearMap.apply 𝕜 𝕜` is injective on `E`. +-/ + +public section + +namespace ContinuousLinearMap + +variable {𝕜 E : Type*} [RCLike 𝕜] + +/-- The evaluation `x ↦ (u ↦ u x)` into the bidual preserves the norm: it is +`NormedSpace.inclusionInDoubleDualLi`, by definition of `NormedSpace.inclusionInDoubleDual`. -/ +theorem norm_apply_apply [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : + ‖ContinuousLinearMap.apply 𝕜 𝕜 x‖ = ‖x‖ := + (NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map x + +/-- The evaluation `x ↦ (u ↦ u x)` into the bidual is injective: it is +`NormedSpace.inclusionInDoubleDualLi`, by definition of `NormedSpace.inclusionInDoubleDual`. -/ +theorem apply_injective [NormedAddCommGroup E] [NormedSpace 𝕜 E] : + Function.Injective (ContinuousLinearMap.apply 𝕜 𝕜 : E → (E →L[𝕜] 𝕜) →L[𝕜] 𝕜) := + (NormedSpace.inclusionInDoubleDualLi 𝕜).injective + +end ContinuousLinearMap