Adds Fenchel conjugates

[ISIPINK]

Builds on PR #252

This is of lower priority as it is not expected to be needed for the learning with expert advice regret proof.

Design Decision

• BddAbove to avoid extended reals

[RemyDegenne]

Do you have an example of development that uses this, on a branch of your fork or elsewhere? It would help judging some design decisions.

[ISIPINK]

Here is an example where I needed Fenchel conjugates, this is a generalization of Lemma 6.39 from Modern Intro to Online Learning version 10, it is about movement bounds /Lipschitzsness of OMD updates.

/--
**Exact Movement Identity with Slack (Minimal Pointwise Formulation)**:

The primal movement divergence `D_ψ(w₂, w₁, gw₁)` is **identically equal** to:
`D_[ψ^*[V]](gw₂ - (δ₁ - δ₂), gw₂, w₂) - Slack`

where `Slack` consists of 4 non-negative components:
1. **Fenchel-Young dual divergence gap at `w₁`**:
   `D_[ψ^*[V]](gw₂ - (δ₁ - δ₂), gw₁, w₁) ≥ 0`
2. **First-order variational optimality at `w₁` tested at `w₂`**:
   `(δ₁ + gφ₁ + gw₁ - gx) (w₂ - w₁) ≥ 0`
3. **First-order variational optimality at `w₂` tested at `w₁`**:
   `(δ₂ + gφ₂ + gw₂ - gx) (w₁ - w₂) ≥ 0`
4. **Regularizer symmetrized divergence**:
   `D_[φ](w₂, w₁, gφ₁) + D_[φ](w₁, w₂, gφ₂) ≥ 0`
-/
theorem movement_eq_dual_bregman_sub_slack (V : Set E) (ψ φ : E → F)
    (w₁ w₂ : E) (gx gw₁ gw₂ δ₁ δ₂ gφ₁ gφ₂ : E →+ F)
    (hgw₁ : gw₁ ∈ ∂[V, w₁] ψ) (hgw₂ : gw₂ ∈ ∂[V, w₂] ψ) :
    D_[ψ](w₂, w₁, gw₁) =
    D_[ψ^*[V]](gw₂ - (δ₁ - δ₂), gw₂, w₂)
    - D_[ψ^*[V]](gw₂ - (δ₁ - δ₂), gw₁, w₁)
    - ( (δ₂ + gφ₂ + gw₂ - gx) (w₁ - w₂)
      + (δ₁ + gφ₁ + gw₁ - gx) (w₂ - w₁)
      + (D_[φ](w₂, w₁, gφ₁) + D_[φ](w₁, w₂, gφ₂)) ) := by
  dsimp [bregmanDivergenceVal, evalBidual]
  simp only [Subdiff.fenchelConjugate hgw₁, Subdiff.fenchelConjugate hgw₂, map_sub]
  abel

Fenchel conjugates will also be handy to characterize closed form solutions from first order conditions see Theorem 6.28 from Modern Intro to Online Learning version 10.

[ISIPINK]

Related: I opened #263 as a draft/roadmap preview of the OCO regret-bound work. The local-norm / Fenchel–Young stability bounding in that branch builds conceptually on the Fenchel conjugates here, so the review order may matter. No action needed here.