def erealDom {F : Type u_2} (f : F → EReal) : Set F

The effective domain dom f of an EReal-valued function, as the set where f is finite (i.e. strictly below ⊤).

Equations

• erealDom f = {x : F | f x < ⊤}

def ProperERealFunction {F : Type u_2} (f : F → EReal) : Prop

A basic notion of properness for an EReal-valued function: it never takes the value ⊥ and is finite at some point.

Equations

• ProperERealFunction f = ((∀ (x : F), f x ≠ ⊥) ∧ ∃ (x : F), f x ≠ ⊤)

def ConvexERealFunction {F : Type u_2} [AddCommGroup F] [Module ℝ F] (f : F → EReal) : Prop

A Jensen-style convexity condition for an EReal-valued function on a real vector space.

Equations

• ConvexERealFunction f = ∀ ⦃x y : F⦄ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ ↑a * f x + ↑b * f y

def ProperConvexERealFunction {F : Type u_2} [AddCommGroup F] [Module ℝ F] (f : F → EReal) : Prop

A "proper convex function" (proper + Jensen convex) for EReal-valued functions.

Equations

• ProperConvexERealFunction f = (ProperERealFunction f ∧ ConvexERealFunction f)

noncomputable def recessionFunctionEReal {F : Type u_2} [AddCommGroup F] (f : F → EReal) : F → EReal

The recession function f₀⁺(y) = sup { f(x+y) - f(x) | x ∈ dom f } for an EReal-valued function.

Equations

• recessionFunctionEReal f y = sSup {r : EReal | ∃ x ∈ erealDom f, r = f (x + y) - f x}

def recessionConeEReal {F : Type u_2} [AddCommGroup F] (f : F → EReal) : Set F

The recession cone {y | f₀⁺(y) ≤ 0} associated to recessionFunctionEReal.

Equations

• recessionConeEReal f = {y : F | recessionFunctionEReal f y ≤ 0}

theorem section14_mem_recessionConeEReal_iff {F : Type u_2} [AddCommGroup F] (g : F → EReal) (y : F) : y ∈ recessionConeEReal g ↔ ∀ x ∈ erealDom g, g (x + y) - g x ≤ 0

Membership in recessionConeEReal is equivalent to a pointwise nonpositivity condition on increment differences over the effective domain.

theorem section14_mem_polarCone_hull_erealDom_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (φ : Module.Dual ℝ E) : φ ∈ polarCone ↑(ConvexCone.hull ℝ (erealDom f)) ↔ ∀ x ∈ erealDom f, φ x ≤ 0

For f : E → EReal, membership in the polar cone of the cone hull of erealDom f is equivalent to being nonpositive on erealDom f.

theorem section14_fenchelConjugate_add_le_of_le_zero_on_dom {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (yStar : Module.Dual ℝ E) (hy : ∀ x ∈ erealDom f, yStar x ≤ 0) (xStar : Module.Dual ℝ E) : fenchelConjugateBilin LinearMap.applyₗ f (xStar + yStar) ≤ fenchelConjugateBilin LinearMap.applyₗ f xStar

If y★ is nonpositive on erealDom f, then the Fenchel conjugate of f is nonincreasing under translation by y★.

theorem section14_eq_coe_of_lt_top {z : EReal} (hzTop : z < ⊤) (hzBot : z ≠ ⊥) : ∃ (r : ℝ), z = ↑r

A finite, non-⊥ EReal value is a real coercion.

theorem section14_fenchelConjugate_ne_bot {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ProperERealFunction f) (xStar : Module.Dual ℝ E) : fenchelConjugateBilin LinearMap.applyₗ f xStar ≠ ⊥

The Fenchel conjugate of a proper function never takes the value ⊥.

theorem section14_step_le_of_mem_recessionCone {F : Type u_2} [AddCommGroup F] (g : F → EReal) {x y : F} (hy : y ∈ recessionConeEReal g) (hx : x ∈ erealDom g) : g (x + y) ≤ g x ∧ x + y ∈ erealDom g

If y ∈ recessionConeEReal g and x ∈ erealDom g, then translating by y does not increase g, and the translate remains in the effective domain.

theorem section14_real_nonpos_of_nat_mul_le (r C : ℝ) (h : ∀ (n : ℕ), ↑n * r ≤ C) : r ≤ 0

If n * r is uniformly bounded above for all natural n, then r ≤ 0.

theorem polar_sum_le_one_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.13 (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 := EuclideanSpace ℝ (Fin n)) C : Set (Module.Dual ℝ _), and we express the coordinate inequalities as φ (EuclideanSpace.single j 1) ≤ 1.

noncomputable def section14_coeffVec (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))) : EuclideanSpace ℝ (Fin 2)

The coefficient vector of a linear functional on ℝ^2 with respect to the standard basis.

Equations

• section14_coeffVec φ = ∑ i : Fin 2, φ (EuclideanSpace.single i 1) • EuclideanSpace.single i 1

noncomputable def section14_C3_center : EuclideanSpace ℝ (Fin 2)

The center (1,0) of the shifted unit disk C₃.

Equations

• section14_C3_center = EuclideanSpace.single 0 1

theorem section14_norm_sq_sub_C3_center (x : EuclideanSpace ℝ (Fin 2)) : ‖x - section14_C3_center‖ ^ 2 = (x.ofLp 0 - 1) ^ 2 + x.ofLp 1 ^ 2

Expanding the squared distance from the center (1,0) gives the defining quadratic inequality for C₃.

theorem section14_mem_C3_iff_norm_sub_le (x : EuclideanSpace ℝ (Fin 2)) : (x.ofLp 0 - 1) ^ 2 + x.ofLp 1 ^ 2 ≤ 1 ↔ ‖x - section14_C3_center‖ ≤ 1

Membership in C₃ is equivalent to being within distance 1 from the center (1,0).

theorem section14_dual_apply_eq_inner_coeffVec (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))) (x : EuclideanSpace ℝ (Fin 2)) : φ x = inner ℝ x (section14_coeffVec φ)

A linear functional on ℝ^2 acts as an inner product with its coefficient vector.

theorem section14_mem_polar_C3_of_le_support_bound (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))) (hφ : φ (EuclideanSpace.single 0 1) + ‖section14_coeffVec φ‖ ≤ 1) : φ ∈ polar {x : EuclideanSpace ℝ (Fin 2) | (x.ofLp 0 - 1) ^ 2 + x.ofLp 1 ^ 2 ≤ 1}

If φ satisfies the support-function bound for the shifted unit disk, then φ belongs to its polar.

theorem section14_support_bound_of_mem_polar_C3 (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))) (hφ : φ ∈ polar {x : EuclideanSpace ℝ (Fin 2) | (x.ofLp 0 - 1) ^ 2 + x.ofLp 1 ^ 2 ≤ 1}) : φ (EuclideanSpace.single 0 1) + ‖section14_coeffVec φ‖ ≤ 1

If φ belongs to the polar of the shifted unit disk, then it satisfies the support-function bound φ(1,0) + ‖vφ‖ ≤ 1.

theorem polar_shiftedUnitDisk_eq : have C₃ := {x : EuclideanSpace ℝ (Fin 2) | (x.ofLp 0 - 1) ^ 2 + x.ofLp 1 ^ 2 ≤ 1}; polar C₃ = {φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2)) | φ (EuclideanSpace.single 0 1) + ‖section14_coeffVec φ‖ ≤ 1}

Text 14.0.14 (Example). Define C₃ = {x = (ξ₁, ξ₂) | (ξ₁ - 1)^2 + ξ₂^2 ≤ 1}. Then its polar can be described as C₃^∘ = {x★ = (ξ₁★, ξ₂★) | ξ₁★ + ‖(ξ₁★, ξ₂★)‖ ≤ 1}.

In this file, C^∘ is modeled as polar (E := EuclideanSpace ℝ (Fin 2)) C : Set (Module.Dual ℝ _), and we interpret the coordinates ξ₁★, ξ₂★ of a functional φ as the values φ (EuclideanSpace.single 0 1) and φ (EuclideanSpace.single 1 1).

theorem section14_counterexample_P_not_subset_polar_C4 : have C₄ := {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 1 - √(1 + x.ofLp 1 ^ 2)}; have P := {φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2)) | √(1 + φ (EuclideanSpace.single 1 1) ^ 2) ≤ φ (EuclideanSpace.single 0 1)}; ¬P ⊆ polar C₄

A concrete counterexample showing that, for the current definition of C₄ and P, the set P is not a subset of the polar C₄^∘. This indicates that polar_C4_eq_convexHull cannot be proven as stated.

@[reducible, inline]

noncomputable abbrev section14_e0 : EuclideanSpace ℝ (Fin 2)

The standard basis vector e₀ in ℝ².

Equations

• section14_e0 = EuclideanSpace.single 0 1

@[reducible, inline]

noncomputable abbrev section14_e1 : EuclideanSpace ℝ (Fin 2)

The standard basis vector e₁ in ℝ².

Equations

• section14_e1 = EuclideanSpace.single 1 1

noncomputable def section14_C4 : Set (EuclideanSpace ℝ (Fin 2))

The set C₄ = {(ξ₁, ξ₂) | ξ₁ ≤ 1 - √(1+ξ₂^2)} from Text 14.0.15.

Equations

• section14_C4 = {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 1 - √(1 + x.ofLp 1 ^ 2)}

noncomputable def section14_P4 : Set (Module.Dual ℝ (EuclideanSpace ℝ (Fin 2)))

The parabola region P₄ = {(a,b) | b^2 + 1 ≤ 2a} in the dual space.

Equations

• section14_P4 = {φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2)) | φ section14_e1 ^ 2 + 1 ≤ 2 * φ section14_e0}

theorem section14_dual_apply_eq_two_coords (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))) (x : EuclideanSpace ℝ (Fin 2)) : φ x = x.ofLp 0 * φ section14_e0 + x.ofLp 1 * φ section14_e1

Coordinate expansion of a linear functional on ℝ².

theorem section14_abs_le_sqrt_one_add_sq (t : ℝ) : |t| ≤ √(1 + t ^ 2)

The basic inequality |t| ≤ √(1+t^2).

theorem section14_sqrt_mul_sub_ge_sqrt_sub {a b t : ℝ} (hb : |b| ≤ a) : √(a ^ 2 - b ^ 2) ≤ a * √(1 + t ^ 2) - b * t

A squaring identity gives the key inequality used in the C₄ polar computation.

theorem section14_convex_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Convex ℝ (polar C)

The polar of any set is convex (as a subset of the dual).

theorem section14_P4_subset_polar_C4 : section14_P4 ⊆ polar section14_C4

The parabola region P₄ is contained in the polar of C₄.

theorem section14_convexHull_P4_union_zero_subset_polar_C4 : (convexHull ℝ) (section14_P4 ∪ {0}) ⊆ polar section14_C4

The easy inclusion conv(P₄ ∪ {0}) ⊆ C₄^∘.

theorem section14_dual_eq_zero_of_apply_e0_e1_eq_zero (φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))) (h0 : φ section14_e0 = 0) (h1 : φ section14_e1 = 0) : φ = 0

A linear functional on ℝ² is determined by its values on the standard basis.

theorem section14_sqrt_one_add_sq_sub_nat_le_inv_nat (n : ℕ) (hn : 1 ≤ n) : √(1 + ↑n ^ 2) - ↑n ≤ 1 / ↑n

A convenient estimate: for n ≥ 1, √(1+n^2) - n ≤ 1/n.

theorem section14_eval_opt_t {a b : ℝ} (ha : 0 ≤ a) (hba : b ^ 2 < a ^ 2) : have t := b / √(a ^ 2 - b ^ 2); a * √(1 + t ^ 2) - b * t = √(a ^ 2 - b ^ 2)

For 0 ≤ a and b^2 < a^2, the choice t = b / √(a^2-b^2) attains the minimum in the expression a * √(1+t^2) - b * t.

theorem section14_mem_polar_C4_coord_consequences {φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2))} (hφ : φ ∈ polar section14_C4) : 0 ≤ φ section14_e0 ∧ |φ section14_e1| ≤ φ section14_e0 ∧ (1 ≤ φ section14_e0 → φ section14_e1 ^ 2 + 1 ≤ 2 * φ section14_e0)

Membership in the polar of C₄ forces the coordinate constraints needed for the description via P₄.

theorem section14_polar_C4_subset_convexHull_P4_union_zero : polar section14_C4 ⊆ (convexHull ℝ) (section14_P4 ∪ {0})

The hard inclusion C₄^∘ ⊆ conv(P₄ ∪ {0}) (to be proven).

theorem polar_C4_eq_convexHull : have C₄ := {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 1 - √(1 + x.ofLp 1 ^ 2)}; have P₄ := {φ : Module.Dual ℝ (EuclideanSpace ℝ (Fin 2)) | φ (EuclideanSpace.single 1 1) ^ 2 + 1 ≤ 2 * φ (EuclideanSpace.single 0 1)}; polar C₄ = (convexHull ℝ) (P₄ ∪ {0})

Text 14.0.15 (Example). Define C₄ = {x = (ξ₁, ξ₂) | ξ₁ ≤ 1 - (1 + ξ₂^2)^{1/2}}. Then its polar can be written as C₄^∘ = conv(P ∪ {0}), where P = {x★ = (ξ₁★, ξ₂★) | ξ₁★ ≥ (1 + (ξ₂★)^2)^{1/2}}.

Note: the set P above (a "sqrt cone") is not contained in the polar for the current definition of polar (via Fenchel conjugates), as shown by section14_counterexample_P_not_subset_polar_C4. The correct description of C₄^∘ in this formalization uses instead the parabola region P₄ = {x★ = (a,b) | b^2 + 1 ≤ 2a}, which is the closed convex hull of all supporting halfspaces through the origin.

In this file, C^∘ is modeled as polar (E := EuclideanSpace ℝ (Fin 2)) C : Set (Module.Dual ℝ _), and we interpret the coordinates ξ₁★, ξ₂★ of a functional φ as the values φ (EuclideanSpace.single 0 1) and φ (EuclideanSpace.single 1 1).