Helper for Text 26.4.0.2: any actual witness of the target conclusion already rules out the
degenerate specialization n = 0 and C = ∅, because that specialization is exactly where the
singleton-space interior-domain contradiction applies.
Helper for Text 26.4.0.2: once the local parameters are specialized to n = 0 and
C = ∅, the exact local existential conclusion of the target theorem is impossible. This
packages the bad case as a direct obstruction for the eventual theorem-level case split.
Helper for Text 26.4.0.2: in zero dimension, any actual witness for the target conclusion
forces the source set to be nonempty, so the repaired theorem statement must exclude the empty
source specialization when n = 0.
Helper for Text 26.4.0.2: in dimension zero, any actual witness of the target conclusion forces the source set to contain a point. This isolates the concrete side condition missing from the current false theorem header.
Helper for Text 26.4.0.2: any actual witness of the target conclusion forces the concrete
zero-dimensional side condition n ≠ 0 ∨ C.Nonempty. This packages the exact local repair that
the obstruction chain isolates.
Helper for Text 26.4.0.2: if the repaired side condition n ≠ 0 ∨ C.Nonempty fails, then
the exact local existential conclusion of the target theorem is impossible.
Helper for Text 26.4.0.2: if the repaired side condition n ≠ 0 ∨ C.Nonempty fails, then
the exact local existential goal type is empty.
Helper for Text 26.4.0.2: the local obstruction splits into a reusable summary. The
declaration-form universal source type is already empty, any actual local witness forces the
repaired side condition n ≠ 0 ∨ C.Nonempty, and failing that side condition empties the exact
local existential goal.
Helper for Text 26.4.0.2: the current theorem hypotheses do not by themselves force the
repaired side condition n ≠ 0 ∨ C.Nonempty; the bad specialization n = 0, C = ∅,
f = 0 still satisfies them.
Helper for Text 26.4.0.2: under the current unrepaired theorem header, the exact local
existential goal has only one formal alternative. Either the repaired side condition
n ≠ 0 ∨ C.Nonempty holds, or the obstruction chain already packages the local goal type as
empty.
Helper for Text 26.4.0.2: transport the openness and differentiability data carried by the
Legendre package from the Euclidean-space coordinates back to the textbook coordinates
Fin n → ℝ.
Helper for Text 26.4.0.2: a proper convex function on all of ℝⁿ can be repackaged as a
proper convex EReal-valued function in the Jensen-style sense used locally in Section 26.
Helper for Text 26.4.0.2: when C = ∅ but n ≠ 0, the indicator of {0} gives an explicit
closed proper convex witness whose effective-domain interior is empty.
Helper for Text 26.4.0.2: transporting the Euclidean-space source function
z ↦ f ((EuclideanSpace.equiv (Fin n) ℝ) z) back to textbook coordinates sends its gradient at
(EuclideanSpace.equiv (Fin n) ℝ).symm x to the Fréchet derivative determined by the transported
coordinate gradient.
Helper for Text 26.4.0.2: transporting the Euclidean-space source function
z ↦ f ((EuclideanSpace.equiv (Fin n) ℝ) z) back to textbook coordinates sends its gradient at
(EuclideanSpace.equiv (Fin n) ℝ).symm x to the coordinate gradient euclideanGradientAt f x.
Helper for Text 26.4.0.2: the closed extension
F = convexFunctionClosure (fun x => (f x : EReal) + indicatorFunction C x) has
euclideanGradientAt f x as a Euclidean subgradient at every x ∈ C.
Helper for Text 26.4.0.2: at each x ∈ C, the closed extension
F = convexFunctionClosure (fun x => (f x : EReal) + indicatorFunction C x) satisfies the
Fenchel-Young equality in the subtraction form used later in the theorem.
Helper for Text 26.4.0.2: at each x ∈ C, the closed extension
F = convexFunctionClosure (fun x => (f x : EReal) + indicatorFunction C x) satisfies the
Fenchel-Young equality at the coordinate gradient euclideanGradientAt f x.
Helper for Text 26.4.0.2: rewriting L.value_eq in textbook coordinates expresses the
Legendre value at a source point as the same subtraction formula that appears in Fenchel-Young.
Text 26.4.0.2: in the Legendre setting of Definition 26.4.0.1, if C is convex and f is
convex on C, and if we exclude the formal degenerate specialization n = 0, C = ∅, then f
admits a closed proper convex EReal-valued extension F on ℝ^n whose effective-domain
interior is exactly C, and the Legendre conjugate g agrees on D with the ordinary Fenchel
conjugate F* of that extension.