noncomputable def instTopologicalSpace_moduleDual_weak {E : Type u_1} [AddCommGroup E] [Module ℝ E] : TopologicalSpace (Module.Dual ℝ E)

The weak topology on the algebraic dual induced by evaluation, used to talk about lower semicontinuity (and hence "closedness") of functions on dual spaces.

def IsProductLowerSemicontinuousBifunction {U : Type u_1} {X : Type u_2} [TopologicalSpace U] [TopologicalSpace X] (F : U → X → EReal) : Prop

A bifunction is "closed" when it is lower semicontinuous as a function on the product.

theorem bifunctionClosure_infimalConvolution_apply_eq_closure_apply_infimalConvolution {m n : ℕ} (F₁ F₂ : FiberwiseProperConvexBifunction m n) (hproper : IsProperEReal fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => bifunctionInfimalConvolution F₁ F₂ p.1 p.2) (hclosed : IsProductLowerSemicontinuousBifunction (bifunctionInfimalConvolution F₁ F₂)) : (∀ u ∈ intrinsicInterior ℝ (bifunctionDom (bifunctionInfimalConvolution F₁ F₂)), bifunctionClosure (bifunctionInfimalConvolution F₁ F₂) u = erealFunctionClosure (bifunctionInfimalConvolution F₁ F₂ u)) ∧ ∀ u ∈ intrinsicInterior ℝ (bifunctionDom F₁.toFun) ∩ intrinsicInterior ℝ (bifunctionDom F₂.toFun), bifunctionClosure (bifunctionInfimalConvolution F₁ F₂) u = erealFunctionClosure (bifunctionInfimalConvolution F₁ F₂ u)

Proposition 38.2.1: We have

(cl (F₁ □ F₂)) u = cl (F₁ u □ F₂ u)

for each u in the relative interior of dom (F₁ □ F₂), and hence in particular for each u ∈ ri (dom F₁) ∩ ri (dom F₂).

Here cl is modeled by bifunctionClosure (closure on the product) on the left-hand side and by erealFunctionClosure (closure on the slice) on the right-hand side, and ri is modeled by intrinsicInterior. Because fiberwise convexity alone gives no regularity in u, the formal statement assumes that the infimal convolution itself is proper and lower semicontinuous on the product.

theorem helperForCorollary_38_2_1_counterexampleFirst_closed : IsProductLowerSemicontinuousBifunction helperForTheorem_38_1_counterexampleFirstBifunction.toFun

Helper for Corollary 38.2.1: the first Section 38.1 counterexample bifunction is already closed in the product sense.

theorem helperForCorollary_38_2_1_counterexampleSecond_closed : IsProductLowerSemicontinuousBifunction helperForTheorem_38_1_counterexampleSecondBifunction.toFun

Helper for Corollary 38.2.1: the constant-zero Section 38.1 counterexample bifunction is closed in the product sense.

theorem helperForCorollary_38_2_1_counterexample_closure_rhs_eq_const_bot : bifunctionClosure (bifunctionInfimalConvolutionInSecond (bifunctionAdjoint helperForTheorem_38_1_counterexampleFirstBifunction.toFun) (bifunctionAdjoint helperForTheorem_38_1_counterexampleSecondBifunction.toFun)) = fun (x x_1 : Module.Dual ℝ (Fin 1 → ℝ)) => ⊥

Helper for Corollary 38.2.1: the closure of the counterexample right-hand side collapses to the constant ⊥ bifunction because the raw function already attains ⊥.

theorem helperForCorollary_38_2_1_counterexample_targetFalse : IsProductLowerSemicontinuousBifunction (bifunctionInfimalConvolution helperForTheorem_38_1_counterexampleFirstBifunction helperForTheorem_38_1_counterexampleSecondBifunction) ∧ bifunctionAdjoint (bifunctionInfimalConvolution helperForTheorem_38_1_counterexampleFirstBifunction helperForTheorem_38_1_counterexampleSecondBifunction) = bifunctionClosure (bifunctionInfimalConvolutionInSecond (bifunctionAdjoint helperForTheorem_38_1_counterexampleFirstBifunction.toFun) (bifunctionAdjoint helperForTheorem_38_1_counterexampleSecondBifunction.toFun)) → False

Helper for Corollary 38.2.1: specializing the claimed conclusion to the Section 38.1 witness pair yields a contradiction.

theorem helperForCorollary_38_2_1_specializedImplicationFalse : ¬(IsProductLowerSemicontinuousBifunction helperForTheorem_38_1_counterexampleFirstBifunction.toFun → IsProductLowerSemicontinuousBifunction helperForTheorem_38_1_counterexampleSecondBifunction.toFun → (intrinsicInterior ℝ (bifunctionDom helperForTheorem_38_1_counterexampleFirstBifunction.toFun) ∩ intrinsicInterior ℝ (bifunctionDom helperForTheorem_38_1_counterexampleSecondBifunction.toFun)).Nonempty → IsProductLowerSemicontinuousBifunction (bifunctionInfimalConvolution helperForTheorem_38_1_counterexampleFirstBifunction helperForTheorem_38_1_counterexampleSecondBifunction) ∧ bifunctionAdjoint (bifunctionInfimalConvolution helperForTheorem_38_1_counterexampleFirstBifunction helperForTheorem_38_1_counterexampleSecondBifunction) = bifunctionClosure (bifunctionInfimalConvolutionInSecond (bifunctionAdjoint helperForTheorem_38_1_counterexampleFirstBifunction.toFun) (bifunctionAdjoint helperForTheorem_38_1_counterexampleSecondBifunction.toFun)))

Helper for Corollary 38.2.1: the full specialized implication is already false on the imported Section 38.1 counterexample pair.

noncomputable def reflectSecondGraphMap {n m : ℕ} : (Fin (n + m) → ℝ) →ₗ[ℝ] Fin (n + m) → ℝ

Corollary 38.2.1: Let F₁ and F₂ be closed proper convex bifunctions from ℝ^m to ℝ^n. If ri (dom F₁) and ri (dom F₂) have a point in common, then F₁ □ F₂ is closed and

(F₁ □ F₂)^* = cl (F₁^* □ F₂^*).

Here cl is modeled by bifunctionClosure, induced from erealFunctionClosure on the product, and the relative interior ri is modeled by intrinsicInterior.

theorem reflectSecondGraphMap_surjective {n m : ℕ} : Function.Surjective ⇑reflectSecondGraphMap

noncomputable def convexReflectionOfConcave {n m : ℕ} (G : (Fin n → ℝ) → (Fin m → ℝ) → EReal) : (Fin n → ℝ) → (Fin m → ℝ) → EReal

theorem convexReflectionOfConcave_graph {n m : ℕ} (G : (Fin n → ℝ) → (Fin m → ℝ) → EReal) : bifunctionGraphFunction (convexReflectionOfConcave G) = fun (z : Fin (n + m) → ℝ) => -bifunctionGraphFunction G (reflectSecondGraphMap z)

theorem convexReflectionOfConcave_properConvexBifunction {n m : ℕ} (G : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hG : ProperConcaveBifunction G) : ProperConvexBifunction (convexReflectionOfConcave G)

theorem fiberwiseProperConvex_of_properConvexBifunction {n m : ℕ} (F : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hF : ProperConvexBifunction F) : ∃ (Fpkg : FiberwiseProperConvexBifunction n m), Fpkg.toFun = F

theorem convexReflectionOfConcave_dom {n m : ℕ} (G : (Fin n → ℝ) → (Fin m → ℝ) → EReal) : bifunctionDom (convexReflectionOfConcave G) = bifunctionDomBot G

theorem neg_iSup_eq_iInf_neg {A : Sort u_1} (f : A → EReal) : -⨆ (a : A), f a = ⨅ (a : A), -f a

theorem iInf_pair_eq_nested {A : Type u_1} {B : Type u_2} (f : A × B → EReal) : ⨅ (p : A × B), f p = ⨅ (a : A), ⨅ (b : B), f (a, b)

theorem textbookBifunctionAdjoint_convexReflection {n m : ℕ} (G : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hG : ConcaveBifunction G) (u : Fin m → ℝ) (x : Fin n → ℝ) : textbookBifunctionAdjoint (convexReflectionOfConcave G) u x = -adjointOfConcaveBifunction ⟨G, hG⟩ u (-x)

theorem infimalConvolution_convexReflection {n m : ℕ} (G₁ G₂ : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (x : Fin n → ℝ) (u : Fin m → ℝ) : bifunctionInfimalConvolutionInSecond (convexReflectionOfConcave G₁) (convexReflectionOfConcave G₂) x u = -concaveBifunctionInfimalConvolutionInSecond G₁ G₂ x (-u)

noncomputable def infimalConvolutionFirstGraphMap {n m : ℕ} : (Fin (n + m + m) → ℝ) →ₗ[ℝ] Fin (n + m) → ℝ

noncomputable def infimalConvolutionSecondGraphMap {n m : ℕ} : (Fin (n + m + m) → ℝ) →ₗ[ℝ] Fin (n + m) → ℝ

theorem infimalConvolutionFirstGraphMap_surjective {n m : ℕ} : Function.Surjective ⇑infimalConvolutionFirstGraphMap

theorem infimalConvolutionSecondGraphMap_surjective {n m : ℕ} : Function.Surjective ⇑infimalConvolutionSecondGraphMap

theorem bifunctionInfimalConvolutionInSecond_convexBifunction {n m : ℕ} (F₁ F₂ : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hF₁ : ProperConvexBifunction F₁) (hF₂ : ProperConvexBifunction F₂) : ConvexBifunction (bifunctionInfimalConvolutionInSecond F₁ F₂)

theorem concaveBifunction_of_convexReflection {n m : ℕ} (G : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hK : ConvexBifunction (convexReflectionOfConcave G)) : ConcaveBifunction G

theorem concaveBifunctionInfimalConvolutionInSecond_concave {n m : ℕ} (G₁ G₂ : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hG₁ : ProperConcaveBifunction G₁) (hG₂ : ProperConcaveBifunction G₂) : ConcaveBifunction (concaveBifunctionInfimalConvolutionInSecond G₁ G₂)

theorem adjointOfConcave_supConvolution_eq_infimalConvolution_adjoint {n m : ℕ} (G₁ G₂ : (Fin n → ℝ) → (Fin m → ℝ) → EReal) (hG₁ : ProperConcaveBifunction G₁) (hG₂ : ProperConcaveBifunction G₂) (hri : (intrinsicInterior ℝ (bifunctionDomBot G₁) ∩ intrinsicInterior ℝ (bifunctionDomBot G₂)).Nonempty) : adjointOfConcaveBifunction ⟨concaveBifunctionInfimalConvolutionInSecond G₁ G₂, ⋯⟩ = bifunctionInfimalConvolutionInSecond (adjointOfConcaveBifunction ⟨G₁, ⋯⟩) (adjointOfConcaveBifunction ⟨G₂, ⋯⟩)

theorem textbookBifunctionAdjoint_eq_adjointOfConvexBifunction {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : ConvexBifunction F) : textbookBifunctionAdjoint F = adjointOfConvexBifunction ⟨F, hF⟩

The textbook bifunction adjoint agrees with the bundled convex-bifunction adjoint.

theorem bifunctionInfimalConvolution_closed_and_adjoint_eq_closure_infimalConvolution_adjoint {m n : ℕ} (F₁ F₂ : FiberwiseProperConvexBifunction m n) (hproper₁ : ProperConvexBifunction F₁.toFun) (hproper₂ : ProperConvexBifunction F₂.toFun) (hclosed₁ : ClosedConvexBifunction F₁.toFun) (hclosed₂ : ClosedConvexBifunction F₂.toFun) (hri : (intrinsicInterior ℝ (bifunctionDomBot (textbookBifunctionAdjoint F₁.toFun)) ∩ intrinsicInterior ℝ (bifunctionDomBot (textbookBifunctionAdjoint F₂.toFun))).Nonempty) : ClosedConvexBifunction (bifunctionInfimalConvolution F₁ F₂) ∧ textbookBifunctionAdjoint (bifunctionInfimalConvolution F₁ F₂) = concaveBifunctionClosure (concaveBifunctionInfimalConvolutionInSecond (textbookBifunctionAdjoint F₁.toFun) (textbookBifunctionAdjoint F₂.toFun))

Corollary 38.2.1: Let F₁ and F₂ be closed proper convex bifunctions from ℝ^m to ℝ^n. If ri (dom F₁*) and ri (dom F₂*) have a point in common, then F₁ □ F₂ is closed and (F₁ □ F₂)* = cl (F₁* □ F₂*).

The adjoints and the closure on the right are the concave bifunction operations used by the book, and ri is represented by intrinsicInterior.

@[reducible, inline]

abbrev FiberwiseConvexBifunction (m n : ℕ) : Type

A convex bifunction from ℝ^m to ℝ^n, bundled with the predicate IsFiberwiseConvexBifunction.

theorem isFiberwiseConvexBifunction_scalarMultiple {m n : ℕ} (F : (Fin m → ℝ) → (Fin n → ℝ) → EReal) (hF : IsFiberwiseConvexBifunction F) (lam : { r : ℝ // 0 < r }) : IsFiberwiseConvexBifunction fun (u : Fin m → ℝ) (x : Fin n → ℝ) => ↑↑lam * F u ((↑lam)⁻¹ • x)

Scalar multiplication preserves convexity of bifunctions in the second variable.

-- Proof sketch: Fix u and apply convexity of the epigraph of x ↦ F u x under the affine change of variables x ↦ λ⁻¹ • x and scaling of function values by the positive scalar λ.

noncomputable def bifunctionScalarMultiple {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) : FiberwiseConvexBifunction m n

Definition 38.2.2: Let F be a convex bifunction from ℝ^m to ℝ^n (modeled here as a FiberwiseConvexBifunction m n). For any scalar λ > 0, the scalar multiple Fλ is defined by (Fλ) u = (F u) λ, i.e.

((Fλ) u) x = λ (F u) (λ⁻¹ x).

theorem isFiberwiseConvexBifunction_convexIndicatorBifunction {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) : IsFiberwiseConvexBifunction (convexIndicatorBifunction A)

Convexity of the convex indicator bifunction in its second variable.

-- Proof sketch: For each fixed u, the slice x ↦ convexIndicatorBifunction A u x is an indicator of a singleton set, whose epigraph is convex; translate this to the epigraph-based predicate IsERealConvex, and hence to IsFiberwiseConvexBifunction.

noncomputable def convexIndicatorFiberwiseConvexBifunction {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) : FiberwiseConvexBifunction m n

The convex indicator bifunction of a linear map, bundled as a FiberwiseConvexBifunction.

theorem helperForProposition_38_2_3_rescaledGraph_iff {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (lam : { r : ℝ // 0 < r }) (u : Fin m → ℝ) (x : Fin n → ℝ) : (↑lam)⁻¹ • x = A u ↔ x = (↑lam • A) u

Helper for Proposition 38.2.3: the rescaled graph condition is equivalent to membership in the graph of the scaled linear map.

theorem helperForProposition_38_2_3_positiveScalar_mul_indicator (lam : { r : ℝ // 0 < r }) (p : Prop) [Decidable p] : (↑↑lam * if p then 0 else ⊤) = if p then 0 else ⊤

Helper for Proposition 38.2.3: multiplying a 0/⊤-valued indicator by a positive finite scalar leaves the indicator unchanged.

theorem bifunctionScalarMultiple_convexIndicatorBifunction {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (lam : { r : ℝ // 0 < r }) : ↑(bifunctionScalarMultiple (convexIndicatorFiberwiseConvexBifunction A) lam) = convexIndicatorBifunction (↑lam • A)

Proposition 38.2.3: If F is the convex indicator bifunction of a linear transformation A : ℝ^m → ℝ^n, then the scalar multiple Fλ (Definition 38.2.2) is the convex indicator bifunction of the scaled linear transformation λ A; equivalently, (Fλ) u = δ(· | { (λ A) u }).

-- Proof sketch: Unfold bifunctionScalarMultiple and convexIndicatorBifunction. For each u, the expression x ↦ λ * (if λ⁻¹ • x = A u then 0 else +∞) is 0 exactly when x = (λ • A) u and +∞ otherwise; rewrite λ⁻¹ • x = A u as x = λ • A u.

noncomputable def bifunctionScalarMultipleInSecond {U : Type u_1} {X : Type u_2} [SMul ℝ X] (F : U → X → EReal) (lam : { r : ℝ // 0 < r }) : U → X → EReal

Scalar multiplication of a raw bifunction in its second variable: (Fλ) u x = λ * F u (λ⁻¹ • x) (with λ > 0 encoded by lam : {r : ℝ // 0 < r}).

theorem helperForTheorem_38_3_positiveScalarMul_continuous (lam : { r : ℝ // 0 < r }) : Continuous fun (z : EReal) => ↑↑lam * z

Helper for Theorem 38.3: multiplication by a fixed positive finite scalar is continuous on EReal.

theorem helperForTheorem_38_3_positiveScalarMul_lowerSemicontinuous {α : Type u_1} [TopologicalSpace α] (lam : { r : ℝ // 0 < r }) (f : α → EReal) (hf : LowerSemicontinuous f) : LowerSemicontinuous fun (x : α) => ↑↑lam * f x

Helper for Theorem 38.3: postcomposing a lower-semicontinuous EReal-valued function with positive scalar multiplication preserves lower semicontinuity.

theorem helperForTheorem_38_3_positiveScalar_mul_finiteAdd (lam : { r : ℝ // 0 < r }) (r : ℝ) (z : EReal) : ↑(↑lam * r) + ↑↑lam * z = ↑↑lam * (↑r + z)

Helper for Theorem 38.3: multiplying a finite real term and an EReal term by a positive scalar distributes over their sum.

theorem helperForTheorem_38_3_positiveScalar_mul_ne_bot (lam : { r : ℝ // 0 < r }) {z : EReal} (hz : z ≠ ⊥) : ↑↑lam * z ≠ ⊥

Helper for Theorem 38.3: multiplying a non-⊥ EReal value by a positive finite scalar cannot produce ⊥.

theorem helperForTheorem_38_3_positiveScalar_mul_ne_top (lam : { r : ℝ // 0 < r }) {z : EReal} (hz : z ≠ ⊤) : ↑↑lam * z ≠ ⊤

Helper for Theorem 38.3: multiplying a non-⊤ EReal value by a positive finite scalar cannot produce ⊤.

theorem helperForTheorem_38_3_positiveScalar_mul_iInf {ι : Sort u_1} (lam : { r : ℝ // 0 < r }) (f : ι → EReal) : ↑↑lam * ⨅ (i : ι), f i = ⨅ (i : ι), ↑↑lam * f i

Helper for Theorem 38.3: multiplying by a fixed positive finite scalar commutes with iInf in EReal.

theorem helperForTheorem_38_3_scalarMultiple_reciprocal_cancel {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) : have lamInv := ⟨(↑lam)⁻¹, ⋯⟩; ↑(bifunctionScalarMultiple (bifunctionScalarMultiple F lam) lamInv) = ↑F

Helper for Theorem 38.3: scaling by λ and then by λ⁻¹ returns the original bifunction.

theorem helperForTheorem_38_3_proper_scalarMultiple_forward {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) (hproper : IsProperEReal fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => ↑F p.1 p.2) : IsProperEReal fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => ↑(bifunctionScalarMultiple F lam) p.1 p.2

Helper for Theorem 38.3: properness on the product is preserved by positive rescaling in the second variable.

theorem helperForTheorem_38_3_productLowerSemicontinuous_scalarMultiple_forward {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) (hclosed : IsProductLowerSemicontinuousBifunction ↑F) : IsProductLowerSemicontinuousBifunction ↑(bifunctionScalarMultiple F lam)

Helper for Theorem 38.3: product lower semicontinuity is preserved by positive rescaling in the second variable.

theorem helperForTheorem_38_3_leftPairing_scalarMultiple {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) (u : Fin m → ℝ) (xStar : Module.Dual ℝ (Fin n → ℝ)) : bifunctionLeftPairing (↑(bifunctionScalarMultiple F lam)) u xStar = ↑↑lam * bifunctionLeftPairing (↑F) u xStar

Helper for Theorem 38.3: the iInf-based left pairing scales by the same positive factor as the bifunction itself.

theorem helperForTheorem_38_3_adjoint_scalarMultiple {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) : bifunctionAdjoint ↑(bifunctionScalarMultiple F lam) = bifunctionScalarMultipleInSecond (bifunctionAdjoint ↑F) lam

Helper for Theorem 38.3: the adjoint of the scaled bifunction is the corresponding positive scalar multiple in the second dual variable.

theorem bifunctionScalarMultiple_closed_iff_and_proper_iff_and_leftPairing_and_adjoint {m n : ℕ} (F : FiberwiseConvexBifunction m n) (lam : { r : ℝ // 0 < r }) : IsFiberwiseConvexBifunction ↑(bifunctionScalarMultiple F lam) ∧ (IsProductLowerSemicontinuousBifunction ↑(bifunctionScalarMultiple F lam) ↔ IsProductLowerSemicontinuousBifunction ↑F) ∧ ((IsProperEReal fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => ↑(bifunctionScalarMultiple F lam) p.1 p.2) ↔ IsProperEReal fun (p : (Fin m → ℝ) × (Fin n → ℝ)) => ↑F p.1 p.2) ∧ (∀ (u : Fin m → ℝ) (xStar : Module.Dual ℝ (Fin n → ℝ)), bifunctionLeftPairing (↑(bifunctionScalarMultiple F lam)) u xStar = ↑↑lam * bifunctionLeftPairing (↑F) u xStar) ∧ bifunctionAdjoint ↑(bifunctionScalarMultiple F lam) = bifunctionScalarMultipleInSecond (bifunctionAdjoint ↑F) lam

Theorem 38.3: Let F be a convex bifunction from ℝ^m to ℝ^n, and let λ > 0. Then Fλ is a convex bifunction; it is closed (resp. proper) if and only if F is closed (resp. proper); and for all u and x* one has ⟨(Fλ) u, x*⟩ = λ ⟨F u, x*⟩. Moreover (Fλ)^* = F^*λ.

noncomputable def bifunctionImage {m n : ℕ} (F : FiberwiseProperConvexBifunction m n) (f : { f : (Fin m → ℝ) → EReal // IsERealConvex f ∧ ∀ (u : Fin m → ℝ), f u ≠ ⊥ }) : (Fin n → ℝ) → EReal

Definition 38.3.1: Let F be a proper convex bifunction from ℝ^m to ℝ^n (here modeled as F : FiberwiseProperConvexBifunction m n, i.e. an EReal-valued bifunction on Fin m → ℝ and Fin n → ℝ that is globally proper and convex in the second variable). Given a convex function f : ℝ^m → EReal which never takes the value -∞, the image Ff is the function on ℝ^n defined by

(Ff) x = inf_u (f u + (F u) x),

modeled in Lean as an iInf over u : Fin m → ℝ. Equivalently, (Ff) x = inf (f - F_* x) where F_* is the inverse bifunctionInverse F.toFun.

noncomputable def linearMapImage {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (f : (Fin m → ℝ) → EReal) : (Fin n → ℝ) → EReal

The image of a function f : ℝ^m → EReal under a linear map A : ℝ^m → ℝ^n, defined by (Af)(x) = inf { f(u) | A u = x }, modeled as an iInf with an indicator (+∞) for the constraint A u = x.

theorem helperForProposition_38_3_2_convexIndicatorSummand_eq_linearImageTerm {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (f : (Fin m → ℝ) → EReal) (u : Fin m → ℝ) (x : Fin n → ℝ) (hf : f u ≠ ⊥) : f u + convexIndicatorBifunction A u x = if A u = x then f u else ⊤

Helper for Proposition 38.3.2: the convex-indicator summand collapses to the constrained linear-image integrand.

theorem helperForProposition_38_3_2_integrand_eq {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (f : { f : (Fin m → ℝ) → EReal // IsERealConvex f ∧ ∀ (u : Fin m → ℝ), f u ≠ ⊥ }) (x : Fin n → ℝ) : (fun (u : Fin m → ℝ) => ↑f u + convexIndicatorBifunction A u x) = fun (u : Fin m → ℝ) => if A u = x then ↑f u else ⊤

Helper for Proposition 38.3.2: after rewriting by the convex indicator bifunction, the whole integrand agrees pointwise with the constrained infimum integrand defining Af.

theorem bifunctionImage_convexIndicatorBifunction_eq_linearMapImage {m n : ℕ} (A : (Fin m → ℝ) →ₗ[ℝ] Fin n → ℝ) (F : FiberwiseProperConvexBifunction m n) (hF : F.toFun = convexIndicatorBifunction A) (f : { f : (Fin m → ℝ) → EReal // IsERealConvex f ∧ ∀ (u : Fin m → ℝ), f u ≠ ⊥ }) : bifunctionImage F f = linearMapImage A ↑f

Proposition 38.3.2: If F is the convex indicator bifunction of a linear transformation A : ℝ^m → ℝ^n, then for any convex function f on ℝ^m that does not take on -∞, the image Ff coincides with the image Af defined by (Af)(x) = inf { f(u) | A u = x }.

noncomputable def fenchelConjugateDual {X : Type u_1} [AddCommMonoid X] [Module ℝ X] (f : X → EReal) : Module.Dual ℝ X → EReal

The Fenchel conjugate f* of an EReal-valued function f : X → EReal, defined on the algebraic dual by f*(x*) = sup_x (⟨x, x*⟩ - f x) where ⟨x, x*⟩ is evaluation.

noncomputable def bifunctionImageRaw {U : Type u_1} {X : Type u_2} (F : U → X → EReal) (f : U → EReal) : X → EReal

The image Ff of a function f under a bifunction F, defined by (Ff)(x) = inf_u (f u + F u x) (modeled by iInf).

theorem helperForTheorem_38_4_identityImage_constZero_eq_constZero : (bifunctionImageRaw (convexIndicatorBifunction LinearMap.id) fun (x : Fin 1 → ℝ) => 0) = fun (x : Fin 1 → ℝ) => 0

Helper for Theorem 38.4: the image of the constant-zero function under the identity graph indicator bifunction is still the constant-zero function.

theorem helperForTheorem_38_4_constZero_conjugateAtZero_eq_zero : fenchelConjugateDual (fun (x : Fin 1 → ℝ) => 0) 0 = 0

Helper for Theorem 38.4: the constant-zero function has conjugate value 0 at the dual origin.

theorem helperForTheorem_38_4_identityLeftSideAtZero_eq_zero : fenchelConjugateDual (bifunctionImageRaw (convexIndicatorBifunction LinearMap.id) fun (x : Fin 1 → ℝ) => 0) 0 = 0

Helper for Theorem 38.4: the left-hand side of the advertised conjugacy formula evaluates to 0 at the dual origin for the identity/constant-zero specialization.

theorem helperForTheorem_38_4_identityQualification : (intrinsicInterior ℝ (erealDom fun (x : Fin 1 → ℝ) => 0) ∩ intrinsicInterior ℝ (bifunctionDom (convexIndicatorBifunction LinearMap.id))).Nonempty

Helper for Theorem 38.4: the identity/constant-zero specialization satisfies the relative interior qualification hypothesis appearing in the theorem statement.

theorem helperForTheorem_38_4_identityRightSideAtZero_eq_bot : bifunctionImageRaw (bifunctionAdjoint (bifunctionInverse (convexIndicatorBifunction LinearMap.id))) (fenchelConjugateDual fun (x : Fin 1 → ℝ) => 0) 0 = ⊥

Helper for Theorem 38.4: on the identity/constant-zero specialization, the right-hand side of the advertised conjugacy formula evaluates to ⊥ at the dual origin.

theorem helperForTheorem_38_4_identitySpecialization_conjugateClauseFalse : ¬((intrinsicInterior ℝ (erealDom fun (x : Fin 1 → ℝ) => 0) ∩ intrinsicInterior ℝ (bifunctionDom (convexIndicatorBifunction LinearMap.id))).Nonempty → fenchelConjugateDual (bifunctionImageRaw (convexIndicatorBifunction LinearMap.id) fun (x : Fin 1 → ℝ) => 0) = bifunctionImageRaw (bifunctionAdjoint (bifunctionInverse (convexIndicatorBifunction LinearMap.id))) (fenchelConjugateDual fun (x : Fin 1 → ℝ) => 0))

Helper for Theorem 38.4: the equality clause in the current theorem statement is already false for the identity graph indicator and the constant-zero function.

theorem helperForTheorem_38_4_identitySpecialization_targetFalse : ¬((intrinsicInterior ℝ (erealDom fun (x : Fin 1 → ℝ) => 0) ∩ intrinsicInterior ℝ (bifunctionDom (convexIndicatorBifunction LinearMap.id))).Nonempty → fenchelConjugateDual (bifunctionImageRaw (convexIndicatorBifunction LinearMap.id) fun (x : Fin 1 → ℝ) => 0) = bifunctionImageRaw (bifunctionAdjoint (bifunctionInverse (convexIndicatorBifunction LinearMap.id))) (fenchelConjugateDual fun (x : Fin 1 → ℝ) => 0) ∧ ∀ (xStar : Module.Dual ℝ (Fin 1 → ℝ)), ∃ (uStar : Module.Dual ℝ (Fin 1 → ℝ)), bifunctionImageRaw (bifunctionAdjoint (bifunctionInverse (convexIndicatorBifunction LinearMap.id))) (fenchelConjugateDual fun (x : Fin 1 → ℝ) => 0) xStar = fenchelConjugateDual (fun (x : Fin 1 → ℝ) => 0) uStar + bifunctionAdjoint (bifunctionInverse (convexIndicatorBifunction LinearMap.id)) uStar xStar)

Helper for Theorem 38.4: the full specialized implication is false because its equality clause already fails at the dual origin.