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

Equations

• section14_instTopologicalSpace_dualWeak_part1 = WeakBilin.instTopologicalSpace LinearMap.applyₗ.flip

def polarCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : Set (Module.Dual ℝ E)

Text 14.0.1: The polar of a non-empty convex cone K is the set Kᵒ = {x★ | ∀ x ∈ K, ⟪x, x★⟫ ≤ 0}.

In this formalization, we interpret x★ as a linear functional Module.Dual ℝ E and the pairing ⟪x, x★⟫ as evaluation x★ x.

Equations

• polarCone K = ↑(PointedCone.dual (-LinearMap.applyₗ) K)

def Set.barrierCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Set (Module.Dual ℝ E)

The barrier cone of a set C is the set of all linear functionals φ that are bounded above on C, i.e. there exists β with φ x ≤ β for every x ∈ C.

Equations

• C.barrierCone = {φ : Module.Dual ℝ E | ∃ (β : ℝ), ∀ x ∈ C, φ x ≤ β}

noncomputable def erealIndicator {E : Type u_1} (K : Set E) : E → EReal

An EReal-valued indicator function: 0 on a set and ⊤ off it.

Equations

• erealIndicator K x = if x ∈ K then 0 else ⊤

noncomputable def fenchelConjugateBilin {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : F → EReal

The (Fenchel–Legendre) conjugate of an EReal-valued function with respect to a bilinear pairing p, defined as sup_x (p x y - f x).

Equations

• fenchelConjugateBilin p f y = sSup (Set.range fun (x : E) => ↑((p x) y) - f x)

theorem mem_dual_neg_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module ℝ F] [ContinuousSMul ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [(-p).IsContPerfPair] (K : ProperCone ℝ E) {y : F} : y ∈ ProperCone.dual (-p) ↑K ↔ ∀ x ∈ ↑K, (p x) y ≤ 0

Membership in the dual cone ProperCone.dual (-p) K is exactly the inequality p x y ≤ 0 for all x ∈ K.

theorem fenchelConjugate_erealIndicator_eq_zero_of_mem_dual {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module ℝ F] [ContinuousSMul ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [(-p).IsContPerfPair] (K : ProperCone ℝ E) {y : F} (hy : y ∈ ProperCone.dual (-p) ↑K) : fenchelConjugateBilin p (erealIndicator ↑K) y = 0

The Fenchel conjugate of the EReal-indicator of a cone is 0 at points in the dual cone.

theorem fenchelConjugate_erealIndicator_eq_top_of_not_mem_dual {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module ℝ F] [ContinuousSMul ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [(-p).IsContPerfPair] (K : ProperCone ℝ E) {y : F} (hy : y ∉ ProperCone.dual (-p) ↑K) : fenchelConjugateBilin p (erealIndicator ↑K) y = ⊤

The Fenchel conjugate of the EReal-indicator of a cone is ⊤ at points outside the dual cone.

theorem fenchelConjugate_erealIndicator_properCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module ℝ F] [ContinuousSMul ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [(-p).IsContPerfPair] (K : ProperCone ℝ E) : fenchelConjugateBilin p (erealIndicator ↑K) = erealIndicator ↑(ProperCone.dual (-p) ↑K)

The Fenchel conjugate of the EReal-indicator of a proper cone is the indicator of the dual cone.

theorem polarCone_polar_polar_eq_and_indicator_conjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [AddCommGroup F] [IsTopologicalAddGroup F] [Module ℝ F] [ContinuousSMul ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [(-p).IsContPerfPair] (K : ProperCone ℝ E) : ((↑(ProperCone.dual (-p) ↑K)).Nonempty ∧ IsClosed ↑(ProperCone.dual (-p) ↑K) ∧ Convex ℝ ↑(ProperCone.dual (-p) ↑K)) ∧ ProperCone.dual (-p).flip ↑(ProperCone.dual (-p) ↑K) = K ∧ fenchelConjugateBilin p (erealIndicator ↑K) = erealIndicator ↑(ProperCone.dual (-p) ↑K) ∧ fenchelConjugateBilin p.flip (erealIndicator ↑(ProperCone.dual (-p) ↑K)) = erealIndicator ↑K

Theorem 14.1: If K is a non-empty closed convex cone, then its polar Kᵒ is also a non-empty closed convex cone and the bipolar identity Kᵒᵒ = K holds. Moreover, the indicator functions of K and Kᵒ are Fenchel–Legendre conjugates of each other.

theorem mem_polarCone_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) (φ : Module.Dual ℝ E) : φ ∈ polarCone K ↔ ∀ x ∈ K, φ x ≤ 0

Membership in polarCone is exactly the pointwise inequality φ x ≤ 0 on the set.

theorem mem_polarCone_submodule_iff_mem_dualAnnihilator {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Submodule ℝ E) (φ : Module.Dual ℝ E) : φ ∈ polarCone ↑K ↔ φ ∈ K.dualAnnihilator

For a submodule K, the polar cone coincides with the dual annihilator.

theorem polarCone_submodule_eq_dualAnnihilator {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Submodule ℝ E) : polarCone ↑K = ↑K.dualAnnihilator

Text 14.0.2: If K is a subspace of ℝ^n, then its polar equals its orthogonal complement: Kᵒ = Kᗮ = {x★ ∈ ℝ^n | ∀ x ∈ K, ⟪x, x★⟫ = 0}.

In this file we interpret Kᵒ as polarCone (K : Set E) (a subset of the dual space Module.Dual ℝ E), and the orthogonal complement as the dual annihilator K.dualAnnihilator = {x★ | ∀ x ∈ K, x★ x = 0}.

def nonposCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (φ : Module.Dual ℝ E) : ConvexCone ℝ E

The convex cone of points where a linear functional is nonpositive.

Equations

• nonposCone φ = { carrier := {x : E | φ x ≤ 0}, smul_mem' := ⋯, add_mem' := ⋯ }

@[simp]

theorem mem_nonposCone_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] (φ : Module.Dual ℝ E) (x : E) : x ∈ nonposCone φ ↔ φ x ≤ 0

theorem hull_le_nonposCone_of_forall_range {E : Type u_1} [AddCommGroup E] [Module ℝ E] {I : Type u_2} (a : I → E) (φ : Module.Dual ℝ E) (h : ∀ (i : I), φ (a i) ≤ 0) : ConvexCone.hull ℝ (Set.range a) ≤ nonposCone φ

If a linear functional is nonpositive on a generating set, it is nonpositive on the cone hull.

theorem le_zero_on_hull_of_le_zero_on_generators {E : Type u_1} [AddCommGroup E] [Module ℝ E] {I : Type u_2} (a : I → E) (φ : Module.Dual ℝ E) (h : ∀ (i : I), φ (a i) ≤ 0) (x : E) : x ∈ ↑(ConvexCone.hull ℝ (Set.range a)) → φ x ≤ 0

If a linear functional is nonpositive on each generator a i, it is nonpositive on the hull.

theorem polarCone_convexConeGenerated_range_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] {I : Type u_2} [Nonempty I] (a : I → E) : polarCone (Set.insert 0 ↑(ConvexCone.hull ℝ (Set.range a))) = {φ : Module.Dual ℝ E | ∀ (i : I), φ (a i) ≤ 0}

Text 14.0.3: If K is the convex cone generated by a non-empty vector collection {a_i | i ∈ I}, then K consists of all non-negative linear combinations of the a_i. Consequently, the polar cone satisfies Kᵒ = {x★ | ∀ x ∈ K, x★ x ≤ 0} = {x★ | ∀ i ∈ I, x★ (a i) ≤ 0}.

theorem mem_polarCone_polar_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) (x : E) : x ∈ PointedCone.dual (-LinearMap.applyₗ).flip (polarCone K) ↔ ∀ (φ : Module.Dual ℝ E), (∀ y ∈ K, φ y ≤ 0) → φ x ≤ 0

Membership in the polar of polarCone K, expressed as a pointwise inequality.

theorem closure_subset_polarCone_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] (K : Set E) : closure K ⊆ ↑(PointedCone.dual (-LinearMap.applyₗ).flip (polarCone K))

If a functional is nonpositive on K, then it is nonpositive on closure K.

theorem polarCone_polar_subset_closure_of_convexCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (K : ConvexCone ℝ E) (hKne : (↑K).Nonempty) : ↑(PointedCone.dual (-LinearMap.applyₗ).flip (polarCone ↑K)) ⊆ closure ↑K

The polar of polarCone K is contained in closure K for a nonempty convex cone K.

theorem polarCone_polar_eq_closure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] [LocallyConvexSpace ℝ E] (K : ConvexCone ℝ E) (hKne : (↑K).Nonempty) : ↑(PointedCone.dual (-LinearMap.applyₗ).flip (polarCone ↑K)) = closure ↑K

Text 14.0.4: The polar of Kᵒ is the closure of K, i.e. (Kᵒ)ᵒ = cl K.

noncomputable def polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Set (Module.Dual ℝ E)

Text 14.0.5: The polar of a non-empty convex set C is C^∘ = {x★ | δ*(x★ | C) - 1 ≤ 0} = {x★ | ∀ x ∈ C, ⟪x, x★⟫ ≤ 1}.

Here we model δ*(x★ | C) as the Fenchel–Legendre conjugate of the EReal-indicator of C with respect to the evaluation pairing.

Equations

• polar C = {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ (erealIndicator C) φ ≤ 1}

theorem section14_le_one_on_C_of_fenchelConjugate_indicator_le_one {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {φ : Module.Dual ℝ E} (hφ : fenchelConjugateBilin LinearMap.applyₗ (erealIndicator C) φ ≤ 1) (x : E) : x ∈ C → φ x ≤ 1

If fenchelConjugateBilin (eval) (erealIndicator C) φ ≤ 1, then φ is bounded above by 1 on C.

theorem section14_fenchelConjugate_indicator_le_one_of_le_one_on_C {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {φ : Module.Dual ℝ E} (hφ : ∀ x ∈ C, φ x ≤ 1) : fenchelConjugateBilin LinearMap.applyₗ (erealIndicator C) φ ≤ 1

If φ is bounded above by 1 on C, then fenchelConjugateBilin (eval) (erealIndicator C) φ ≤ 1.

theorem mem_polar_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {φ : Module.Dual ℝ E} : φ ∈ polar C ↔ ∀ x ∈ C, φ x ≤ 1

Text 14.0.5 (membership form): x★ ∈ C^∘ iff ⟪x, x★⟫ ≤ 1 for all x ∈ C.

theorem section14_le_one_of_mem_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {φ : Module.Dual ℝ E} (hφ : φ ∈ polar C) (x : E) : x ∈ C → φ x ≤ 1

If φ ∈ polar C, then φ is bounded above by 1 on C.

This is a convenient lemma for Text 14.0.6 that avoids unfolding mem_polar_iff.

theorem section14_fenchelConjugate_gauge_eq_zero_of_mem_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hCabs : Absorbent ℝ C) {φ : Module.Dual ℝ E} (hφ : φ ∈ polar C) : fenchelConjugateBilin LinearMap.applyₗ (fun (x : E) => ↑(gauge C x)) φ = 0

If φ ∈ polar C and C is absorbent, then fenchelConjugateBilin (eval) (gauge C) φ = 0.

theorem section14_fenchelConjugate_gauge_eq_top_of_not_mem_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {φ : Module.Dual ℝ E} (hφ : φ ∉ polar C) : fenchelConjugateBilin LinearMap.applyₗ (fun (x : E) => ↑(gauge C x)) φ = ⊤

If φ ∉ polar C, then fenchelConjugateBilin (eval) (gauge C) φ = ⊤.

theorem section14_fenchelConjugate_gauge_eq_erealIndicator_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hCabs : Absorbent ℝ C) : (fenchelConjugateBilin LinearMap.applyₗ fun (x : E) => ↑(gauge C x)) = erealIndicator (polar C)

The Fenchel conjugate of the (real-valued) gauge is the EReal indicator of polar C, assuming C is absorbent.

theorem fenchelBiconjugate_gauge_eq_fenchelConjugate_indicator_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hCabs : Absorbent ℝ C) : have p := LinearMap.applyₗ; fenchelConjugateBilin p.flip (fenchelConjugateBilin p fun (x : E) => ↑(gauge C x)) = fenchelConjugateBilin p.flip (erealIndicator (polar C))

Text 14.0.6: Let C be a non-empty convex set. Then the closure cl γ(·|C) of the gauge equals the support function δ*(·|C^∘) of the polar set.

In this file we model γ(·|C) as mathlib's gauge C, and we model the closure operation cl as the Fenchel–Legendre biconjugate with respect to the evaluation pairing. We model δ*(·|C^∘) as the Fenchel–Legendre conjugate of the EReal-indicator of polar C with respect to the flipped evaluation pairing.

Note: mathlib's gauge C is real-valued, so to match the intended convex-analytic gauge (which may take the value ⊤ when C does not absorb directions), we explicitly assume C is absorbent.

theorem section14_polarCone_eq_iInter {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : polarCone K = ⋂ x ∈ K, {φ : Module.Dual ℝ E | φ x ≤ 0}

polarCone K is an intersection of pointwise half-spaces.

theorem section14_isClosed_polarCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : IsClosed (polarCone K)

polarCone is closed in the weak topology on Module.Dual.

theorem section14_convex_polarCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : Convex ℝ (polarCone K)

polarCone is convex (as a subset of the dual space).

theorem section14_zero_mem_polarCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : 0 ∈ polarCone K

The zero functional always belongs to the polar cone.

theorem isClosed_convex_polarCone_and_zero_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : ConvexCone ℝ E) : IsClosed (polarCone ↑K) ∧ Convex ℝ (polarCone ↑K) ∧ 0 ∈ polarCone ↑K

Text 14.0.7. Let K be a non-empty convex cone in ℝ^n. Then the polar cone Kᵒ defined in Text 14.0.1 is a closed convex cone containing the origin.

In this file, Kᵒ is modeled as polarCone (E := E) (K : Set E), a subset of the dual space Module.Dual ℝ E.

theorem section14_polarCone_antitone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {A B : Set E} (hAB : A ⊆ B) : polarCone B ⊆ polarCone A

polarCone is order-reversing: enlarging the set shrinks its polar cone.

theorem section14_polarCone_subset_polarCone_closure {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] (K : Set E) : polarCone K ⊆ polarCone (closure K)

If every linear functional is continuous (e.g. in finite dimension), then polar membership extends from a set to its topological closure.

theorem polarCone_closure_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] (K : ConvexCone ℝ E) : polarCone (closure ↑K) = polarCone ↑K

Text 14.0.8. Let K be a non-empty convex cone in ℝ^n. Then the polar of cl K coincides with the polar of K, i.e. (cl K)^∘ = K^∘. In this file, we express this using the polar cone polarCone (Text 14.0.1): polarCone (closure K) = polarCone K.

def normalConeAtOrigin {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Set (Module.Dual ℝ E)

The normal cone to a set C at the origin, modeled in the dual space: N(0 | C).

Equations

• normalConeAtOrigin C = {φ : Module.Dual ℝ E | ∀ x ∈ C, φ x ≤ 0}

def normalConeAtOriginDual {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set (Module.Dual ℝ E)) : Set E

The normal cone to a set C in the dual space at the origin, modeled in the primal space: N(0 | C).

Equations

• normalConeAtOriginDual C = {x : E | ∀ φ ∈ C, φ x ≤ 0}

theorem section14_polarCone_eq_normalConeAtOrigin {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : polarCone K = normalConeAtOrigin K

The polar cone agrees with the normal cone to the set at the origin (in the dual space).

theorem section14_normalConeAtOriginDual_eq_pointedCone_dual_flip {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set (Module.Dual ℝ E)) : normalConeAtOriginDual C = ↑(PointedCone.dual (-LinearMap.applyₗ).flip C)

The normal cone at the origin in the primal agrees with the dual cone defined via evaluation.

theorem polarCone_eq_normalConeAtOrigin_and_normalConeAtOriginDual_polarCone_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] [LocallyConvexSpace ℝ E] (K : ConvexCone ℝ E) (hKne : (↑K).Nonempty) (hKclosed : IsClosed ↑K) : polarCone ↑K = normalConeAtOrigin ↑K ∧ ↑K = normalConeAtOriginDual (polarCone ↑K)

Text 14.0.9. Let K be a non-empty closed convex cone in ℝ^n. Then the polar cone K^∘ consists of all vectors normal to K at the origin, and conversely K consists of all vectors normal to K^∘ at the origin. Equivalently, writing N(0 | C) for the normal cone of C at 0, one has K^∘ = N(0 | K) and K = N(0 | K^∘).

In this file, K^∘ is modeled by polarCone (E := E) (K : Set E). The normal cone at 0 is modeled by normalConeAtOrigin (in the dual) and normalConeAtOriginDual (in the primal).

theorem section14_mem_pointedConeDual_negInner_iff (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (y : EuclideanSpace ℝ (Fin n)) : y ∈ ↑(PointedCone.dual (-innerₗ (EuclideanSpace ℝ (Fin n))) K) ↔ ∀ x ∈ K, inner ℝ x y ≤ 0

Unpack membership in the dual cone w.r.t. the pairing -(innerₗ _).

theorem section14_coord_nonpos_of_mem_dual_nonnegOrthant (n : ℕ) (y : EuclideanSpace ℝ (Fin n)) (hy : y ∈ ↑(PointedCone.dual (-innerₗ (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i})) (i : Fin n) : y.ofLp i ≤ 0

A vector in the dual cone of the nonnegative orthant has all coordinates nonpositive.

theorem section14_mem_neg_nonnegOrthant_iff_coord_nonpos (n : ℕ) (y : EuclideanSpace ℝ (Fin n)) : y ∈ -{x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i} ↔ ∀ (i : Fin n), y.ofLp i ≤ 0

Membership in the negation of the nonnegative orthant is coordinatewise nonpositivity.

theorem section14_inner_nonpos_of_coords_nonneg_nonpos (n : ℕ) (x y : EuclideanSpace ℝ (Fin n)) (hx : ∀ (i : Fin n), 0 ≤ x.ofLp i) (hy : ∀ (i : Fin n), y.ofLp i ≤ 0) : inner ℝ x y ≤ 0

If x has nonnegative coordinates and y has nonpositive coordinates, then ⟪x, y⟫ ≤ 0.

theorem polarCone_nonnegOrthant_eq_neg (n : ℕ) : ↑(PointedCone.dual (-innerₗ (EuclideanSpace ℝ (Fin n))) {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i}) = -{x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 ≤ x.ofLp i}

Text 14.0.10. Let K ⊆ ℝ^n be the non-negative orthant K = {x = (ξ₁, …, ξₙ) | ξⱼ ≥ 0 for j = 1, …, n}. Then the polar cone of K is the non-positive orthant, i.e. K^∘ = -K.

In Lean, we model ℝ^n as EuclideanSpace ℝ (Fin n) and the polar cone as the dual cone with respect to the pairing -(innerₗ _), so that y is in the polar cone of K iff ⟪x, y⟫ ≤ 0 for all x ∈ K.

theorem polar_antitone_of_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {C₁ C₂ : Set E} (hC : C₁ ⊆ C₂) : polar C₂ ⊆ polar C₁

Text 14.0.11. Polarity is order-inverting: if C₁ ⊆ C₂ are closed convex sets containing the origin, then their polars satisfy C₁^∘ ⊇ C₂^∘.

In this file, C^∘ is modeled as polar (E := E) C.

theorem section14_dual_apply_eq_sum_mul_single {n : ℕ} (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin n)) : φ x = ∑ i : Fin n, x.ofLp i * φ (EuclideanSpace.single i 1)

A linear functional on ℝ^n is determined by its values on the coordinate vectors.

theorem section14_single_one_mem_subprobabilitySimplex (n : ℕ) (j : Fin n) : EuclideanSpace.single j 1 ∈ {x : EuclideanSpace ℝ (Fin n) | (∀ (j : Fin n), 0 ≤ x.ofLp j) ∧ ∑ j : Fin n, x.ofLp j ≤ 1}

Each coordinate vector e_j belongs to the subprobability simplex {x | x ≥ 0, ∑ x ≤ 1}.

theorem section14_le_one_of_forall_single_le_one_and_mem_C₁ {n : ℕ} (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin n)) (hφ : ∀ (j : Fin n), φ (EuclideanSpace.single j 1) ≤ 1) (hxnonneg : ∀ (j : Fin n), 0 ≤ x.ofLp j) (hxsum : ∑ j : Fin n, x.ofLp j ≤ 1) : φ x ≤ 1

If φ is bounded by 1 on all coordinate vectors, then it is bounded by 1 on C₁.

theorem polar_subprobabilitySimplex_eq (n : ℕ) : have C₁ := {x : EuclideanSpace ℝ (Fin n) | (∀ (j : Fin n), 0 ≤ x.ofLp j) ∧ ∑ j : Fin n, x.ofLp j ≤ 1}; polar C₁ = {φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin n)) | ∀ (j : Fin n), φ (EuclideanSpace.single j 1) ≤ 1}

Text 14.0.12 (Example). Define C₁ = {x = (ξ₁, …, ξₙ) | ξⱼ ≥ 0, ξ₁ + ⋯ + ξₙ ≤ 1}. Then its polar is C₁^∘ = {x★ = (ξ₁★, …, ξₙ★) | ξⱼ★ ≤ 1 for j = 1, …, n}.

In this file, C^∘ is modeled as polar (E := E) C : Set (Module.Dual ℝ E). For ℝ^n we use E = EuclideanSpace ℝ (Fin n), and we express the coordinate inequalities as φ (Pi.single j 1) ≤ 1.