def IsSingleValuedMultivaluedMap {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : Prop

Definition 26.0.1: a multivalued mapping ρ is single-valued if for every x, the value ρ x contains at most one point.

def inverseMultivaluedMap {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : Y → Set X

Definition 26.0.2: the inverse multivalued mapping of ρ sends x* to the set of all x such that x* ∈ ρ(x).

def IsOneToOneMultivaluedMap {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : Prop

Definition 26.0.3: a multivalued mapping ρ is one-to-one precisely when both ρ and its inverse multivalued mapping ρ⁻¹ are single-valued.

def multivaluedMapGraph {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : Set (X × Y)

The graph of a multivalued mapping ρ consists of the pairs (x, y) with y ∈ ρ x.

theorem helperForLemma_26_1_graphMembership_iff {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) (x : X) (y : Y) : (x, y) ∈ multivaluedMapGraph ρ ↔ y ∈ ρ x

Helper for Lemma 26.1: membership in the graph of ρ is exactly membership in the fiber ρ x.

theorem helperForLemma_26_1_graphFiberUniqueness_iff_singleValued {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : IsSingleValuedMultivaluedMap ρ ↔ ∀ ⦃x : X⦄ ⦃y₁ y₂ : Y⦄, (x, y₁) ∈ multivaluedMapGraph ρ → (x, y₂) ∈ multivaluedMapGraph ρ → y₁ = y₂

Helper for Lemma 26.1: single-valuedness of ρ is equivalent to uniqueness of the second coordinate inside each graph fiber over a fixed x.

theorem helperForLemma_26_1_swappedGraphFiberUniqueness_iff_inverseSingleValued {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : IsSingleValuedMultivaluedMap (inverseMultivaluedMap ρ) ↔ ∀ ⦃x₁ x₂ : X⦄ ⦃y : Y⦄, (x₁, y) ∈ multivaluedMapGraph ρ → (x₂, y) ∈ multivaluedMapGraph ρ → x₁ = x₂

Helper for Lemma 26.1: single-valuedness of ρ⁻¹ is equivalent to uniqueness of the first coordinate inside each graph fiber over a fixed x*.

theorem isOneToOneMultivaluedMap_iff_graph_coordinate_uniqueness {X : Type u_1} {Y : Type u_2} (ρ : X → Set Y) : IsOneToOneMultivaluedMap ρ ↔ (∀ ⦃x : X⦄ ⦃y₁ y₂ : Y⦄, (x, y₁) ∈ multivaluedMapGraph ρ → (x, y₂) ∈ multivaluedMapGraph ρ → y₁ = y₂) ∧ ∀ ⦃x₁ x₂ : X⦄ ⦃y : Y⦄, (x₁, y) ∈ multivaluedMapGraph ρ → (x₂, y) ∈ multivaluedMapGraph ρ → x₁ = x₂

Lemma 26.1: a multivalued mapping ρ is one-to-one exactly when its graph contains neither two distinct pairs with the same first coordinate nor two distinct pairs with the same second coordinate.

def HasSingleValuedInjectiveSubdifferential {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

The convex-analytic condition that the subdifferential of f is single-valued on its effective domain and injective there.

def legendreGradientImage {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ) : Set (EuclideanSpace ℝ (Fin n))

The gradient image of C under f, which is the dual domain used in the Legendre conjugate construction.

theorem mem_legendreGradientImage {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ} {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ C) : gradient f x ∈ legendreGradientImage C f

Every gradient value of a point of C lies in the gradient image of C.

structure LegendreConjugateOn {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ) : Type

Definition 26.4.0.1: the Legendre conjugate of a differentiable real-valued function f on an open set C ⊆ ℝ^n is the pair (D, g) where D is the image of C under the gradient map ∇ f, and g is the real-valued function on D given by g (xStar) = ⟪(∇ f)⁻¹ xStar, xStar⟫ - f ((∇ f)⁻¹ xStar). The field fiber_well_defined records the weaker hypothesis from the text ensuring that this formula is independent of the chosen preimage in a gradient fiber, so injectivity of ∇ f is not assumed in the definition.

• isOpen_source : IsOpen C
• differentiableOn_source : DifferentiableOn ℝ f C
• conjFun : ↑(legendreGradientImage C f) → ℝ
• fiber_well_defined ⦃x₁ x₂ xStar : EuclideanSpace ℝ (Fin n)⦄ : x₁ ∈ C → x₂ ∈ C → gradient f x₁ = xStar → gradient f x₂ = xStar → x₁.ofLp ⬝ᵥ xStar.ofLp - f x₁ = x₂.ofLp ⬝ᵥ xStar.ofLp - f x₂
• value_eq ⦃x : EuclideanSpace ℝ (Fin n)⦄ (hx : x ∈ C) : self.conjFun ⟨gradient f x, ⋯⟩ = ((fun (i : Fin n) => x.ofLp i) ⬝ᵥ fun (i : Fin n) => (gradient f x).ofLp i) - f x

structure LegendreConjugatePackageOn {X : Type u_1} {Y : Type u_2} (pair : X → Y → ℝ) (C : Set X) (f : X → EReal) : Type (max u_1 u_2)

Auxiliary package recording a Legendre-conjugate construction relative to a chosen pairing and a chosen map on the source set.

• target : Set Y
• conjFun : Y → EReal
• toFun : X → Y
• image_eq : self.target = self.toFun '' C
• fiber_well_defined ⦃x₁ x₂ : X⦄ ⦃xStar : Y⦄ : x₁ ∈ C → x₂ ∈ C → self.toFun x₁ = xStar → self.toFun x₂ = xStar → ↑(pair x₁ xStar) - f x₁ = ↑(pair x₂ xStar) - f x₂
• value_eq ⦃x : X⦄ : x ∈ C → self.conjFun (self.toFun x) = ↑(pair x (self.toFun x)) - f x

@[reducible, inline]

abbrev LegendreTransformationOn {n : ℕ} (C : Set (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ) : Type

Definition 26.4.0.2: passing from (C, f) to its well-defined Legendre conjugate (D, g) is called the Legendre transformation. In the Euclidean differentiable setting fixed in Definition 26.4.0.1, this is exactly the same data as a LegendreConjugateOn C f.

noncomputable def interiorGradientMap {n : ℕ} (f : (Fin n → ℝ) → EReal) (hdiff : ∀ x ∈ interior (effectiveDomain Set.univ f), ERealDifferentiableAt f x) : (Fin n → ℝ) → Fin n → ℝ

The chosen gradient on int (dom f) for an EReal-valued function that is differentiable at every interior effective-domain point, extended by 0 outside that interior.

theorem helperForText_26_4_0_2_effectiveDomain_univ_finZero {F : (Fin 0 → ℝ) → EReal} (hF : ProperERealFunction F) : effectiveDomain Set.univ F = Set.univ

Helper for Text 26.4.0.2: on the singleton space Fin 0 → ℝ, properness forces the effective domain on univ to be all of space.

theorem helperForText_26_4_0_2_interior_effectiveDomain_univ_finZero {F : (Fin 0 → ℝ) → EReal} (hF : ProperConvexERealFunction F) : interior (effectiveDomain Set.univ F) = Set.univ

Helper for Text 26.4.0.2: any proper convex extension on Fin 0 → ℝ has full interior effective domain, so it cannot realize C = ∅.

theorem helperForText_26_4_0_2_interior_effectiveDomain_nonempty_finZero {F : (Fin 0 → ℝ) → EReal} (hF : ProperConvexERealFunction F) : (interior (effectiveDomain Set.univ F)).Nonempty

Helper for Text 26.4.0.2: on Fin 0 → ℝ, the interior effective domain of a proper convex extension is nonempty.

theorem helperForText_26_4_0_2_interior_effectiveDomain_ne_empty_finZero {F : (Fin 0 → ℝ) → EReal} (hF : ProperConvexERealFunction F) : interior (effectiveDomain Set.univ F) ≠ ∅

Helper for Text 26.4.0.2: for a fixed proper convex function on Fin 0 → ℝ, the interior effective domain cannot be empty.

theorem helperForText_26_4_0_2_no_emptyInteriorExtension_finZero : ¬∃ (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ interior (effectiveDomain Set.univ F) = ∅

Helper for Text 26.4.0.2: on Fin 0 → ℝ, the conclusion interior (effectiveDomain F) = ∅ cannot hold for a proper convex extension.

theorem helperForText_26_4_0_2_legendreGradientImage_empty {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} : legendreGradientImage ∅ f = ∅

Helper for Text 26.4.0.2: the gradient image of the empty source set is empty.

theorem helperForText_26_4_0_2_false_of_mem_emptyGradientImage {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {xStar : EuclideanSpace ℝ (Fin n)} (hxStar : xStar ∈ legendreGradientImage ∅ f) : False

Helper for Text 26.4.0.2: no point lies in the gradient image of the empty source set.

theorem helperForText_26_4_0_2_differentiableOn_empty_finZero {f : EuclideanSpace ℝ (Fin 0) → ℝ} : DifferentiableOn ℝ f ∅

Helper for Text 26.4.0.2: every function is differentiable on the empty zero-dimensional source set.

def helperForText_26_4_0_2_emptyGradientImageConjFun_finZero {f : EuclideanSpace ℝ (Fin 0) → ℝ} : ↑(legendreGradientImage ∅ f) → ℝ

Helper for Text 26.4.0.2: the conjugate function on the empty gradient image is the unique function out of that empty target type.

theorem helperForText_26_4_0_2_emptyFiberWellDefined_finZero {f : EuclideanSpace ℝ (Fin 0) → ℝ} ⦃x₁ x₂ xStar : EuclideanSpace ℝ (Fin 0)⦄ : x₁ ∈ ∅ → x₂ ∈ ∅ → gradient f x₁ = xStar → gradient f x₂ = xStar → x₁.ofLp ⬝ᵥ xStar.ofLp - f x₁ = x₂.ofLp ⬝ᵥ xStar.ofLp - f x₂

Helper for Text 26.4.0.2: fiber well-definedness is vacuous on the empty zero-dimensional source set.

theorem helperForText_26_4_0_2_emptyValueEq_finZero {f : EuclideanSpace ℝ (Fin 0) → ℝ} ⦃x : EuclideanSpace ℝ (Fin 0)⦄ (hx : x ∈ ∅) : helperForText_26_4_0_2_emptyGradientImageConjFun_finZero ⟨gradient f x, ⋯⟩ = ((fun (i : Fin 0) => x.ofLp i) ⬝ᵥ fun (i : Fin 0) => (gradient f x).ofLp i) - f x

Helper for Text 26.4.0.2: the Legendre value formula is vacuous on the empty zero-dimensional source set.

def helperForText_26_4_0_2_emptyLegendreTransformationSource_finZero {f : EuclideanSpace ℝ (Fin 0) → ℝ} : LegendreTransformationOn ∅ f

Helper for Text 26.4.0.2: in the zero-dimensional empty-source case, there is an explicit vacuous Legendre-transformation package on the empty source set.

theorem helperForText_26_4_0_2_nonemptyLegendreTransformation_finZero {f : EuclideanSpace ℝ (Fin 0) → ℝ} : Nonempty (LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) f)

Helper for Text 26.4.0.2: after simplifying the image of ∅, the zero-dimensional Legendre-transformation hypothesis is inhabited.

theorem helperForText_26_4_0_2_counterexampleHypotheses_finZero {f : (Fin 0 → ℝ) → ℝ} : Convex ℝ ∅ ∧ ConvexOn ℝ ∅ f ∧ Nonempty (LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x))

Helper for Text 26.4.0.2: the specialization n = 0, C = ∅ really satisfies every hypothesis of the target theorem before the contradiction in the conclusion appears.

theorem helperForText_26_4_0_2_emptyConclusionImpossible_finZero {f : (Fin 0 → ℝ) → ℝ} (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x)) : ¬∃ (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ ∅, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = ∅ ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate 0 F (↑xStar).ofLp

Helper for Text 26.4.0.2: once specialized to n = 0 and C = ∅, the theorem's conclusion contradicts proper convexity before the Fenchel-conjugate clause is used.

theorem helperForText_26_4_0_2_emptyConclusionTypeIsEmpty_finZero {f : (Fin 0 → ℝ) → ℝ} (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x)) : IsEmpty (∃ (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ ∅, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = ∅ ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate 0 F (↑xStar).ofLp)

Helper for Text 26.4.0.2: for a fixed zero-dimensional empty-source Legendre datum, the specialized conclusion type is empty.

theorem helperForText_26_4_0_2_emptyCaseTheoremShapeFalse {f : (Fin 0 → ℝ) → ℝ} (hEmptyCase : ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x)), ∃ (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ ∅, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = ∅ ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => f ((EuclideanSpace.equiv (Fin 0) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate 0 F (↑xStar).ofLp) : False

Helper for Text 26.4.0.2: the theorem shape already fails in the specialization n = 0, C = ∅, before any universal quantification over dimensions is considered.

theorem helperForText_26_4_0_2_zeroFunctionCounterexampleWitness_finZero : ∃ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => (fun (x : Fin 0 → ℝ) => 0) ((EuclideanSpace.equiv (Fin 0) ℝ) x)), ¬∃ (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ ∅, F x = ↑((fun (x : Fin 0 → ℝ) => 0) x)) ∧ interior (effectiveDomain Set.univ F) = ∅ ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => (fun (x : Fin 0 → ℝ) => 0) ((EuclideanSpace.equiv (Fin 0) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate 0 F (↑xStar).ofLp

Helper for Text 26.4.0.2: the concrete specialization n = 0, C = ∅, f = 0 already refutes the theorem's local conclusion shape.

theorem helperForText_26_4_0_2_zeroFunctionEmptyCaseFalse : ¬∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => (fun (x : Fin 0 → ℝ) => 0) ((EuclideanSpace.equiv (Fin 0) ℝ) x)), ∃ (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ ∅, F x = ↑((fun (x : Fin 0 → ℝ) => 0) x)) ∧ interior (effectiveDomain Set.univ F) = ∅ ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => (fun (x : Fin 0 → ℝ) => 0) ((EuclideanSpace.equiv (Fin 0) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate 0 F (↑xStar).ofLp

Helper for Text 26.4.0.2: the concrete specialization n = 0, C = ∅, f = 0 already refutes the theorem's local conclusion shape.

theorem helperForText_26_4_0_2_specializedWitness_finZero (hTarget : ∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) : ∃ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => (fun (x : Fin 0 → ℝ) => 0) ((EuclideanSpace.equiv (Fin 0) ℝ) x)) (F : (Fin 0 → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ ∅, F x = ↑((fun (x : Fin 0 → ℝ) => 0) x)) ∧ interior (effectiveDomain Set.univ F) = ∅ ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin 0) ℝ).symm '' ∅) fun (x : EuclideanSpace ℝ (Fin 0)) => (fun (x : Fin 0 → ℝ) => 0) ((EuclideanSpace.equiv (Fin 0) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate 0 F (↑xStar).ofLp

Helper for Text 26.4.0.2: any proof of the theorem's universal statement yields the forbidden zero-dimensional extension data after specializing to n = 0 and C = ∅.

theorem helperForText_26_4_0_2_specializedWitnessImpossible_finZero (hTarget : ∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) : False

Helper for Text 26.4.0.2: the specialized zero-dimensional witness extracted from any putative universal proof is already impossible, because its conclusion forces empty interior effective domain on a singleton space.

theorem helperForText_26_4_0_2_universalStatementContradiction (hTarget : ∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) : False

Helper for Text 26.4.0.2: the theorem's full universal shape is refuted by the zero-dimensional empty-set specialization.

theorem helperForText_26_4_0_2_targetStatement_iff_declarationSignature : (∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) ↔ ∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: the curried universal theorem shape and the declaration-form signature are equivalent presentations of the same statement.

theorem helperForText_26_4_0_2_targetStatementIsEmpty : IsEmpty (∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp)

Helper for Text 26.4.0.2: the curried universal theorem statement is empty for the same zero-dimensional empty-set reason as the declaration-form signature.

theorem helperForText_26_4_0_2_targetStatementFalse : ¬∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: the full universally quantified theorem statement is false, because the specialization n = 0, C = ∅ satisfies the hypotheses but violates the conclusion.

theorem helperForText_26_4_0_2_false_of_declarationSignature_finZero (hDecl : ∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) (f : (Fin 0 → ℝ) → ℝ) : False

Helper for Text 26.4.0.2: any declaration-form proof specializes to the impossible zero-dimensional empty-set case, for every f : (Fin 0 → ℝ) → ℝ.

theorem helperForText_26_4_0_2_declarationSignatureFalse : ¬∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: the theorem's declaration-form signature is already refuted by the same zero-dimensional empty-set specialization.

theorem helperForText_26_4_0_2_declarationSignatureIsEmpty : IsEmpty (∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp)

Helper for Text 26.4.0.2: the exact declaration type of the target theorem is empty, because the zero-dimensional empty-set specialization already contradicts it.

theorem helperForText_26_4_0_2_localGoal_of_declarationSignature {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC_convex : Convex ℝ C) (hf_convex : ConvexOn ℝ C f) (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)) (hDecl : ∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) : ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: any inhabitant of the declaration-form universal statement would specialize immediately to the current local theorem goal.

theorem helperForText_26_4_0_2_localReductionRouteData {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC_convex : Convex ℝ C) (hf_convex : ConvexOn ℝ C f) (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)) : IsEmpty (∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) ∧ ((∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) → ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp)

Helper for Text 26.4.0.2: for the current local parameters, the remaining declaration-based proof skeleton is completely explicit. The exact declaration signature is empty, but any repaired inhabitant of that signature would specialize to the present local goal.

theorem helperForText_26_4_0_2_noLocalDeclarationSignature {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC_convex : Convex ℝ C) (hf_convex : ConvexOn ℝ C f) (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)) : ¬∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: in the current local theorem context, the exact declaration-form source type is still uninhabited, so no proof can be obtained merely by specializing the current false universal header.

theorem helperForText_26_4_0_2_noLocalDeclarationSpecializationPair {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC_convex : Convex ℝ C) (hf_convex : ConvexOn ℝ C f) (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)) : IsEmpty ((∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) ∧ ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp)

Helper for Text 26.4.0.2: in the current local theorem context, there cannot simultaneously be a declaration-form universal proof term and a witness for the present goal, because the declaration-form source type is already empty.

theorem helperForText_26_4_0_2_localWitness_blocks_declarationRoute {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC_convex : Convex ℝ C) (hf_convex : ConvexOn ℝ C f) (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)) : (∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) → ¬∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: once a local witness for the present goal is fixed, the declaration-form universal route is still unavailable, because combining the two would inhabit the already-empty specialization pair type.

theorem helperForText_26_4_0_2_localGoalRouteSummary {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} (hC_convex : Convex ℝ C) (hf_convex : ConvexOn ℝ C f) (L : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)) : ((∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) → ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp) ∧ ¬∀ {n : ℕ} {C : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ}, Convex ℝ C → ConvexOn ℝ C f → ∀ (L' : LegendreTransformationOn (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x)), ∃ (F : (Fin n → ℝ) → EReal), ProperConvexERealFunction F ∧ LowerSemicontinuous F ∧ (∀ x ∈ C, F x = ↑(f x)) ∧ interior (effectiveDomain Set.univ F) = C ∧ ∀ (xStar : ↑(legendreGradientImage (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C) fun (x : EuclideanSpace ℝ (Fin n)) => f ((EuclideanSpace.equiv (Fin n) ℝ) x))), ↑(L'.conjFun xStar) = fenchelConjugate n F (↑xStar).ofLp

Helper for Text 26.4.0.2: in the current local theorem context, the exact local goal is what any repaired declaration-form proof would specialize to, but the declaration-form source type is already empty. This isolates the remaining blocker to an upstream repair of the theorem statement rather than to any further local decomposition.