Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A finite maximum of affine functions and its active subgradients

Example

Let n,m≥1, let a1,…,am∈Rn, and let b1,…,bm∈R. Define f:Rn→R by

f(x)=max⁡1≤j≤m(⟨aj,x⟩+bj),

and let J(x)={j:f(x)=⟨aj,x⟩+bj} be the active index set. Then f is convex and

∂f(x)=conv⁡{aj:j∈J(x)}.

For the two-dimensional function f(x1,x2)=max⁡{x1,−x1,x2,−x2}, the subdifferential at zero is conv⁡{±e1,±e2}={v:∣v1∣+∣v2∣≤1}.

Facts & Assumptions

Given: The affine family above, subgradients as in Subgradients and the subdifferential of a convex function, and finite convex combinations as in Finite Jensen inequality for convex functions on Rn.

[L1]

The pointwise maximum of a nonempty finite family of convex functions on a common convex domain is convex (Nonnegative combinations, affine precomposition, and finite pointwise maxima preserve convexity).

[L2]

A point outside a nonempty closed convex set is strictly separated from it (A point outside a nonempty closed convex set is strictly separated from it).

[L3]

For positive Euclidean dimension, a subset is compact if and only if it is closed and bounded (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L4]

The continuous image of a compact subset is compact (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L5]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).

Verification

technique · direct
1.1

Each affine constituent is convex, so [L1] makes their nonempty finite maximum f convex.

L1
2.1

If j∈J(x), then f(y)≥⟨aj,y⟩+bj=f(x)+⟨aj,y−x⟩. Nonnegative weighted sums of these inequalities show that every convex combination of active slopes is a subgradient.

step 1.1algebra
3.1

The active-weight simplex is closed and bounded, hence compact by [L3]; its affine image is compact by [L4] and closed by [L5]. If a subgradient v lay outside this active convex hull, [L2] would give a direction h with ⟨v,h⟩ strictly larger than every active ⟨aj,h⟩. Finiteness lets one choose t>0 small enough that inactive affine pieces remain below the active maximum at x+th. Then the subgradient inequality would require an increment at least t⟨v,h⟩, while the actual increment is tmax⁡j∈J(x)⟨aj,h⟩, a contradiction. The displayed four-piece formula follows from its four active slopes at zero.

step 2.1L2L3L4L5algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

46 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources