theorem helperForLemma_31_0_12_counterexample_dualSup_eq_zero : ⨆ (xStar : Fin 1 → ℝ), fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) xStar - fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => 0) xStar = 0

Helper for Lemma 31.0.12: in the one-dimensional counterexample, the left-hand dual supremum is exactly 0. The origin contributes 0, while every nonzero dual vector contributes ⊥ because the conjugate of the constant-zero function is the singleton indicator at the origin.

theorem helperForLemma_31_0_12_targetHeaderSpecializesToZeroEqBot (hFenchel : ∀ {n : ℕ} (f g : (Fin n → ℝ) → EReal), ProperConvexFunctionOn Set.univ f → ClosedConvexFunction f → ClosedERealFunction g → (∀ (x : Fin n → ℝ), g x ≠ ⊥) → (effectiveDomain Set.univ f ∩ effectiveDomain Set.univ g).Nonempty ∨ (effectiveDomain Set.univ (fenchelConjugate n f) ∩ effectiveDomain Set.univ (fenchelConjugate n g)).Nonempty → ⨆ (xStar : Fin n → ℝ), fenchelConjugate n g xStar - fenchelConjugate n f xStar = Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ∧ Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ≤ translatedDifferenceValueFunction f g 0 ∧ translatedDifferenceValueFunction f g 0 = functionInfimumEReal fun (x : Fin n → ℝ) => f x - g x) : 0 = ⊥

Helper for Lemma 31.0.12: any proof of the current theorem schema specializes to the explicit counterexample and forces the impossible identity 0 = ⊥.

theorem helperForLemma_31_0_12_counterexampleLeadingEqualityFalse : ¬⨆ (xStar : Fin 1 → ℝ), fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) xStar - fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => 0) xStar = Filter.liminf (translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) (nhds 0)

Helper for Lemma 31.0.12: the one-dimensional quadratic/zero counterexample already falsifies the leading equality claimed in the target theorem.

theorem helperForLemma_31_0_12_counterexampleTailRelationsHold : Filter.liminf (translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) (nhds 0) ≤ translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) 0 ∧ translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) 0 = functionInfimumEReal fun (x : Fin 1 → ℝ) => 0 - ↑(x 0 ^ 2)

Helper for Lemma 31.0.12: the one-dimensional quadratic/zero counterexample still satisfies the valid tail inequalities liminf p ≤ p(0) and p(0) = inf_x (f x - g x), so the obstruction is isolated to the leading equality.

theorem helperForLemma_31_0_12_counterexampleFullConclusionFalse : ¬(⨆ (xStar : Fin 1 → ℝ), fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) xStar - fenchelConjugate 1 (fun (x : Fin 1 → ℝ) => 0) xStar = Filter.liminf (translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) (nhds 0) ∧ Filter.liminf (translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) (nhds 0) ≤ translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) 0 ∧ translatedDifferenceValueFunction (fun (x : Fin 1 → ℝ) => 0) (fun (x : Fin 1 → ℝ) => ↑(x 0 ^ 2)) 0 = functionInfimumEReal fun (x : Fin 1 → ℝ) => 0 - ↑(x 0 ^ 2))

Helper for Lemma 31.0.12: the one-dimensional quadratic/zero counterexample falsifies the entire displayed conclusion, even though the tail inequalities remain valid there.

theorem helperForLemma_31_0_12_targetHeaderSchemaIsFalse : ¬∀ {n : ℕ} (f g : (Fin n → ℝ) → EReal), ProperConvexFunctionOn Set.univ f → ClosedConvexFunction f → ClosedERealFunction g → (∀ (x : Fin n → ℝ), g x ≠ ⊥) → (effectiveDomain Set.univ f ∩ effectiveDomain Set.univ g).Nonempty ∨ (effectiveDomain Set.univ (fenchelConjugate n f) ∩ effectiveDomain Set.univ (fenchelConjugate n g)).Nonempty → ⨆ (xStar : Fin n → ℝ), fenchelConjugate n g xStar - fenchelConjugate n f xStar = Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ∧ Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ≤ translatedDifferenceValueFunction f g 0 ∧ translatedDifferenceValueFunction f g 0 = functionInfimumEReal fun (x : Fin n → ℝ) => f x - g x

Helper for Lemma 31.0.12: the explicit quadratic/zero counterexample refutes the current universal theorem schema, so no local proof can exist until the leading equality is repaired.

noncomputable def helperForLemma_31_0_12_currentHeaderCounterexampleF : (Fin 1 → ℝ) → EReal

Helper for Lemma 31.0.12: the direct counterexample to the current theorem header uses the singleton indicator at the origin as the convex function f.

noncomputable def helperForLemma_31_0_12_currentHeaderCounterexampleG : (Fin 1 → ℝ) → EReal

Helper for Lemma 31.0.12: the direct counterexample to the current theorem header uses the quadratic function x ↦ (x 0)^2 as g.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_satisfiesTargetHypotheses : ProperConvexFunctionOn Set.univ helperForLemma_31_0_12_currentHeaderCounterexampleF ∧ ClosedConvexFunction helperForLemma_31_0_12_currentHeaderCounterexampleF ∧ ClosedERealFunction helperForLemma_31_0_12_currentHeaderCounterexampleG ∧ (∀ (x : Fin 1 → ℝ), helperForLemma_31_0_12_currentHeaderCounterexampleG x ≠ ⊥) ∧ ((effectiveDomain Set.univ helperForLemma_31_0_12_currentHeaderCounterexampleF ∩ effectiveDomain Set.univ helperForLemma_31_0_12_currentHeaderCounterexampleG).Nonempty ∨ (effectiveDomain Set.univ (fenchelConjugate 1 helperForLemma_31_0_12_currentHeaderCounterexampleF) ∩ effectiveDomain Set.univ (fenchelConjugate 1 helperForLemma_31_0_12_currentHeaderCounterexampleG)).Nonempty)

Helper for Lemma 31.0.12: the explicit indicator/quadratic pair already satisfies the actual current theorem hypotheses, so any obstruction must come from the theorem conclusion itself.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_affineMinusQuadratic_hasNoRealLowerBound (xStar : Fin 1 → ℝ) : ¬HasRealLowerBound fun (x : Fin 1 → ℝ) => ↑(x ⬝ᵥ xStar) - helperForLemma_31_0_12_currentHeaderCounterexampleG x

Helper for Lemma 31.0.12: for every dual vector x⋆, the affine perturbation x ↦ ⟪x, x⋆⟫ - (x 0)^2 is unbounded below on ℝ^1.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_concaveConjugate_eq_bot (xStar : Fin 1 → ℝ) : concaveFenchelConjugate helperForLemma_31_0_12_currentHeaderCounterexampleG xStar = ⊥

Helper for Lemma 31.0.12: the concave conjugate of the quadratic counterexample is ⊥ everywhere, because each affine-minus-quadratic slice is unbounded below.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_indicatorConjugate_eq_zero : fenchelConjugate 1 helperForLemma_31_0_12_currentHeaderCounterexampleF = fun (x : Fin 1 → ℝ) => 0

Helper for Lemma 31.0.12: the Fenchel conjugate of the singleton indicator counterexample is the constant-zero function.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_dualSup_eq_bot : ⨆ (xStar : Fin 1 → ℝ), fenchelDualObjective helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG xStar = ⊥

Helper for Lemma 31.0.12: in the actual current theorem header, the direct indicator/quadratic counterexample has dual supremum ⊥.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_translatedValue_eq_negSquare (u : Fin 1 → ℝ) : translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG u = ↑(-u 0 ^ 2)

Helper for Lemma 31.0.12: for the direct indicator/quadratic counterexample, the translated value function is the negative square u ↦ -(u 0)^2.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_liminf_eq_zero : Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0) = 0

Helper for Lemma 31.0.12: the liminf side of the actual current theorem header evaluates to 0 on the direct indicator/quadratic counterexample.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_dualSupAndLiminfValues : ⨆ (xStar : Fin 1 → ℝ), fenchelDualObjective helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG xStar = ⊥ ∧ Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0) = 0

Helper for Lemma 31.0.12: the direct indicator/quadratic counterexample evaluates the two sides of the disputed leading equality to the incompatible constants ⊥ and 0.

theorem helperForLemma_31_0_12_currentHeaderCounterexampleTailRelationsHold : Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0) ≤ translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG 0 ∧ translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG 0 = functionInfimumEReal fun (x : Fin 1 → ℝ) => helperForLemma_31_0_12_currentHeaderCounterexampleF x - helperForLemma_31_0_12_currentHeaderCounterexampleG x

Helper for Lemma 31.0.12: the valid tail relations liminf p ≤ p(0) and p(0) = inf_x (f x - g x) still hold for the direct indicator/quadratic counterexample used against the current theorem header.

theorem helperForLemma_31_0_12_currentHeaderCounterexample_dualSup_ne_liminf : ⨆ (xStar : Fin 1 → ℝ), fenchelDualObjective helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG xStar ≠ Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0)

Helper for Lemma 31.0.12: the direct indicator/quadratic counterexample already falsifies the leading equality in the actual current theorem header.

theorem helperForLemma_31_0_12_currentHeaderCounterexampleLeadingEqualityFalse : ¬⨆ (xStar : Fin 1 → ℝ), fenchelDualObjective helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG xStar = Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0)

Helper for Lemma 31.0.12: the direct indicator/quadratic counterexample already falsifies the leading equality in the actual current theorem header.

theorem helperForLemma_31_0_12_currentHeaderCounterexampleFullConclusionFalse : ¬(⨆ (xStar : Fin 1 → ℝ), fenchelDualObjective helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG xStar = Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0) ∧ Filter.liminf (translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG) (nhds 0) ≤ translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG 0 ∧ translatedDifferenceValueFunction helperForLemma_31_0_12_currentHeaderCounterexampleF helperForLemma_31_0_12_currentHeaderCounterexampleG 0 = functionInfimumEReal fun (x : Fin 1 → ℝ) => helperForLemma_31_0_12_currentHeaderCounterexampleF x - helperForLemma_31_0_12_currentHeaderCounterexampleG x)

Helper for Lemma 31.0.12: for the direct indicator/quadratic counterexample, the full current theorem conclusion is false even though the tail relations remain valid.

theorem helperForLemma_31_0_12_currentHeaderSchemaIsFalse : ¬∀ {n : ℕ} (f g : (Fin n → ℝ) → EReal), ProperConvexFunctionOn Set.univ f → ClosedConvexFunction f → ClosedERealFunction g → (∀ (x : Fin n → ℝ), g x ≠ ⊥) → (effectiveDomain Set.univ f ∩ effectiveDomain Set.univ g).Nonempty ∨ (effectiveDomain Set.univ (fenchelConjugate n f) ∩ effectiveDomain Set.univ (fenchelConjugate n g)).Nonempty → ⨆ (xStar : Fin n → ℝ), fenchelDualObjective f g xStar = Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ∧ Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ≤ translatedDifferenceValueFunction f g 0 ∧ translatedDifferenceValueFunction f g 0 = functionInfimumEReal fun (x : Fin n → ℝ) => f x - g x

Helper for Lemma 31.0.12: the actual current theorem schema is already refuted by the direct indicator/quadratic counterexample, so no proof can exist without repairing the statement upstream.

theorem fenchelDualSupremum_eq_liminf_translatedDifferenceValueFunction_le_at_zero {n : ℕ} (f g : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) (hg : ProperConcaveFunctionOn Set.univ g) (hclosed : ClosedConvexFunction f ∧ ClosedConcaveFunction g) (hdom : (effectiveDomain Set.univ f ∩ concaveEffectiveDomain g).Nonempty ∨ (effectiveDomain Set.univ (fenchelConjugate n f) ∩ concaveConjugateEffectiveDomain g).Nonempty) : ⨆ (xStar : Fin n → ℝ), fenchelDualObjective f g xStar = Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ∧ Filter.liminf (translatedDifferenceValueFunction f g) (nhds 0) ≤ translatedDifferenceValueFunction f g 0 ∧ translatedDifferenceValueFunction f g 0 = functionInfimumEReal fun (x : Fin n → ℝ) => f x - g x

Lemma 31.0.12 (Inequality Between the Dual Objective and p(u)): let f : ℝ^n → ℝ ∪ {+∞} be proper convex and let g : ℝ^n → ℝ ∪ {-∞} be proper concave. Assume f and g are closed, and either dom f ∩ dom g ≠ ∅ or dom f⋆ ∩ dom g⋆ ≠ ∅, encoded here by the nonemptiness of effectiveDomain ∩ concaveEffectiveDomain or of effectiveDomain(f⋆) ∩ concaveConjugateEffectiveDomain(g). For the translated value function p(u) = inf_x (f x - g (x + u)), represented by translatedDifferenceValueFunction f g, one has sup_xStar φ(xStar) = liminf_{u → 0} p(u) ≤ p(0) = inf_x (f x - g x), where φ = fenchelDualObjective f g.