theorem section16_fenchelConjugate_sum_eq_infimalConvolutionFamily_of_nonempty_iInter_ri_effectiveDomain_proof_step {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i))).Nonempty) : ((fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) ∧ ∀ (xStar : Fin n → ℝ), infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar = ⊤ ∨ ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, fenchelConjugate n (f i) (xStarFamily i) = infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar

Remove both closures under the ri hypothesis and record attainment.

theorem section16_fenchelConjugate_sum_eq_infimalConvolutionFamily_of_nonempty_iInter_ri_effectiveDomain {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i))).Nonempty) : ((fenchelConjugate n fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x) = infimalConvolutionFamily fun (i : Fin m) => fenchelConjugate n (f i)) ∧ ∀ (xStar : Fin n → ℝ), infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar = ⊤ ∨ ∃ (xStarFamily : Fin m → Fin n → ℝ), ∑ i : Fin m, xStarFamily i = xStar ∧ ∑ i : Fin m, fenchelConjugate n (f i) (xStarFamily i) = infimalConvolutionFamily (fun (i : Fin m) => fenchelConjugate n (f i)) xStar

Theorem 16.4.3 (sum vs infimal convolution without closures).

theorem section16_le_zero_of_forall_pos_add_mul_le {a b : ℝ} (h : ∀ (t : ℝ), 0 < t → a + t * b ≤ 0) : a ≤ 0

If a + t * b ≤ 0 for all positive t, then a ≤ 0.

theorem section16_iInter_polar_subset_polar_sum {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) : ⋂ (i : Fin m), {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0} ⊆ {xStar : Fin n → ℝ | ∀ x ∈ ∑ i : Fin m, ↑(K i), x ⬝ᵥ xStar ≤ 0}

The intersection of the polars is contained in the polar of the sum.

theorem section16_polar_sum_subset_iInter_polar {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) (hKne : ∀ (i : Fin m), (↑(K i)).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ ∑ i : Fin m, ↑(K i), x ⬝ᵥ xStar ≤ 0} ⊆ ⋂ (i : Fin m), {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0}

The polar of the sum is contained in the intersection of the polars.

theorem section16_polar_sum_convexCones {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) (hKne : ∀ (i : Fin m), (↑(K i)).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ ∑ i : Fin m, ↑(K i), x ⬝ᵥ xStar ≤ 0} = ⋂ (i : Fin m), {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0}

Corollary 16.4.2.1: Let K₁, …, Kₘ be non-empty convex cones in ℝⁿ. Then the polar cone of their Minkowski sum is the intersection of their polar cones:

(K₁ + ⋯ + Kₘ)^∘ = K₁^∘ ∩ ⋯ ∩ Kₘ^∘.

theorem section16_innerDual_neg_eq_neg_innerDual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : Set H) : ↑(ProperCone.innerDual (-s)) = -↑(ProperCone.innerDual s)

Negating a set flips the inner dual cone.

theorem section16_inner_polar_eq_neg_innerDual {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : Set H) : {y : H | ∀ x ∈ s, inner ℝ x y ≤ 0} = -↑(ProperCone.innerDual s)

The inner-product polar set is the negation of the inner dual cone.

theorem section16_inner_polar_polar_eq_closure_convexCone {n : ℕ} (K : ConvexCone ℝ (EuclideanSpace ℝ (Fin n))) (hKne : (↑K).Nonempty) : {xStar : EuclideanSpace ℝ (Fin n) | ∀ x ∈ {z : EuclideanSpace ℝ (Fin n) | ∀ x ∈ ↑K, inner ℝ x z ≤ 0}, inner ℝ x xStar ≤ 0} = closure ↑K

The double inner-product polar of a convex cone is its closure.

theorem section16_polar_polar_eq_closure_convexCone {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) (hKne : (↑K).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ {z : Fin n → ℝ | ∀ x ∈ ↑K, x ⬝ᵥ z ≤ 0}, x ⬝ᵥ xStar ≤ 0} = closure ↑K

The dot-product double polar of a convex cone is its closure.

theorem section16_polar_sum_polars_eq_iInter_closure {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) (hKne : ∀ (i : Fin m), (↑(K i)).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ ∑ i : Fin m, {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0}, x ⬝ᵥ xStar ≤ 0} = ⋂ (i : Fin m), closure ↑(K i)

The polar of the sum of polars is the intersection of the closures.

theorem section16_polar_polar_sum_polars_eq_closure_sum_polars {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) : {xStar : Fin n → ℝ | ∀ x ∈ {y : Fin n → ℝ | ∀ z ∈ ∑ i : Fin m, {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0}, z ⬝ᵥ y ≤ 0}, x ⬝ᵥ xStar ≤ 0} = closure (∑ i : Fin m, {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0})

The double polar of the sum of polars is the closure of that sum.

theorem section16_polar_iInter_closure_eq_closure_sum_polars {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) (hKne : ∀ (i : Fin m), (↑(K i)).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ ⋂ (i : Fin m), closure ↑(K i), x ⬝ᵥ xStar ≤ 0} = closure (∑ i : Fin m, {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0})

Corollary 16.4.2.2. Let K₁, …, Kₘ be non-empty convex cones in ℝⁿ. Then (cl K₁ ∩ ⋯ ∩ cl Kₘ)^∘ = cl (K₁^∘ + ⋯ + Kₘ^∘).

In this development, cl is closure, ∩ is ⋂, and K^∘ is represented as the set {xStar | ∀ x ∈ K, ⟪x, xStar⟫ ≤ 0}.

theorem section16_supportFunctionEReal_convexCone_eq_indicatorFunction_polar {n : ℕ} (K : ConvexCone ℝ (Fin n → ℝ)) (hKne : (↑K).Nonempty) : supportFunctionEReal ↑K = indicatorFunction {xStar : Fin n → ℝ | ∀ x ∈ ↑K, x ⬝ᵥ xStar ≤ 0}

The support function of a nonempty convex cone is the indicator of its polar.

theorem section16_set_eq_of_indicatorFunction_eq {n : ℕ} {A B : Set (Fin n → ℝ)} (h : indicatorFunction A = indicatorFunction B) : A = B

Indicator functions determine their sets.

theorem section16_polar_iInter_eq_sum_polars_of_nonempty_iInter_ri {n m : ℕ} (K : Fin m → ConvexCone ℝ (Fin n → ℝ)) (hKne : ∀ (i : Fin m), (↑(K i)).Nonempty) (hri : (⋂ (i : Fin m), euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' ↑(K i))).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ ⋂ (i : Fin m), ↑(K i), x ⬝ᵥ xStar ≤ 0} = ∑ i : Fin m, {xStar : Fin n → ℝ | ∀ x ∈ ↑(K i), x ⬝ᵥ xStar ≤ 0}

Corollary 16.4.2.3: Let K₁, …, Kₘ be non-empty convex cones in ℝⁿ. If the cones ri Kᵢ, i = 1, …, m, have a point in common, then

(K₁ ∩ ⋯ ∩ Kₘ)^∘ = (K₁^∘ + ⋯ + Kₘ^∘).

In this development, K^∘ is represented as the set {xStar | ∀ x ∈ K, ⟪x, xStar⟫ ≤ 0} and ri is euclideanRelativeInterior.