Documentation

Tdaf.Analysis.Convex.Duality.ConcaveOps

Supremal convolution and the conjugate of a concave sum #

Two convex functions are combined by infimal convolution f₁ □ f₂, and the conjugate of a sum is that convolution. Two concave functions are combined by supremal convolution (g □ h)(x) = sup {g x₁ + h x₂ ∣ x₁ + x₂ = x}, and the concave conjugate of a sum is that: the concave orientation of the same duality, which the adjoint of F₁ □ F₂ needs.

Main definitions #

Main results #

Implementation notes #

supConv negates values, not arguments, so it inherits commutativity, associativity and the effective-domain formula from infConv. The reflection of the argument that does appear, infConv_neg, comes from the sign dictionary neg_concaveConj, which reflects on the dual side; the proof of the concave conjugate formula crosses it once.

The two properness fields of IsExactSum B (-g₁) (-g₂) say exactly that neither gᵢ takes the value +∞, which is where the classical proof case-splits; the relative-interior condition supplies the third field (IsExactSum.of_relint). No case distinction survives into the statement.

References #

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §16 and §38.

EReal bookkeeping #

source
theorem Tdaf.ConvexAnalysis.neg_add_of_ne_bot {u v : EReal} (hu : u ≠ ⊥) (hv : v ≠ ⊥) :
-(u + v) = -u + -v

Negation distributes over an EReal sum as soon as neither summand is ⊥: the mirror of Tdaf.EReal.neg_add_of_ne_top, and with it the whole sign dictionary for sums.

Infimal convolution and reflection #

source
theorem Tdaf.ConvexAnalysis.infConv_neg {E : Type u_1} [AddCommGroup E] (f g : E → EReal) (x : E) :
infConv (fun (w : E) => f (-w)) (fun (w : E) => g (-w)) x = infConv f g (-x)

Infimal convolution commutes with negating the argument: (f ∘ -) □ (g ∘ -) = (f □ g) ∘ -. Negation in the first coordinate is an additive bijection of E × ℝ, so it carries the sum of the epigraphs to the sum of their images.

Supremal convolution #

source
noncomputable def Tdaf.ConvexAnalysis.supConv {E : Type u_1} [AddCommGroup E] (g h : E → EReal) :
E → EReal

Supremal convolution of two concave functions, Rockafellar's □ in its concave orientation: (g □ h)(x) = sup {g x₁ + h x₂ | x₁ + x₂ = x}. Defined as -((-g) □ (-h)), so that every property of infConv transfers by one negation; the supremum formula is supConv_apply.

Equations
Instances For
    source
    theorem Tdaf.ConvexAnalysis.supConv_def {E : Type u_1} [AddCommGroup E] (g h : E → EReal) :
    supConv g h = fun (x : E) => -infConv (fun (w : E) => -g w) (fun (w : E) => -h w) x
    source
    @[simp]
    theorem Tdaf.ConvexAnalysis.neg_supConv {E : Type u_1} [AddCommGroup E] (g h : E → EReal) (x : E) :
    -supConv g h x = infConv (fun (w : E) => -g w) (fun (w : E) => -h w) x
    source
    theorem Tdaf.ConvexAnalysis.supConv_comm {E : Type u_1} [AddCommGroup E] (g h : E → EReal) :
    supConv g h = supConv h g
    source
    theorem Tdaf.ConvexAnalysis.supConv_apply {E : Type u_1} [AddCommGroup E] {g h : E → EReal} (hg : ∀ (x : E), g x ≠ ⊤) (hh : ∀ (x : E), h x ≠ ⊤) (x : E) :
    supConv g h x = ⨆ (y : E), g (x - y) + h y

    The formula for the concave □: (g □ h)(x) = sup {g (x - y) + h y | y}. The hypotheses mirror those of infConv_apply: without them the summand is ∞ - ∞ where one function is +∞ and the other -∞, and EReal resolves it on the wrong side.

    The concave conjugate of a sum #

    source
    theorem Tdaf.ConvexAnalysis.concaveConj_add_of_isExactSum {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g₁ g₂ : E → EReal} (hex : IsExactSum B (fun (x : E) => -g₁ x) fun (x : E) => -g₂ x) :
    (concaveConj B fun (x : E) => g₁ x + g₂ x) = supConv (concaveConj B g₁) (concaveConj B g₂)

    The conjugate of a concave sum: the concave conjugate of a sum is the supremal convolution of the concave conjugates, (g₁ + g₂)* = g₁* □ g₂*.

    The hypothesis is the convex IsExactSum interface applied to -g₁ and -g₂.