theorem eventually_of_forall {α : Type u_1} {l : Filter α} {p : α → Prop} (hp : ∀ (x : α), p x) : Filter.Eventually p l

A pointwise true predicate holds eventually.

theorem lineSet_unbounded : ¬Bornology.IsBounded {x : Fin 2 → ℝ | ∃ (t : ℝ), x = ![1, 0] + t • ![0, 1]}

The vertical line {(1, t)} is unbounded.

theorem recC_closedBall_eq_zero : have C := Metric.closedBall ![1, 0] ‖![1, 0]‖; have e := EuclideanSpace.equiv (Fin 2) ℝ; have C' := ⇑e.symm '' C; have recC := ⇑e '' C'.recessionCone; recC = {0}

The recession cone of the closed ball centered at ![1, 0] is {0}.

theorem cone_closedBall_imp_pos_first {x : Fin 2 → ℝ} (hx : x ∈ convexConeGenerated 2 (Metric.closedBall ![1, 0] ‖![1, 0]‖)) (hx0 : x ≠ 0) : 0 ≤ x 0

Nonzero points in the cone over the closed ball centered at ![1, 0] have positive first coordinate.

theorem pos_first_mem_cone_closedBall {x : Fin 2 → ℝ} (hx : 0 < x 0) : x ∈ convexConeGenerated 2 (Metric.closedBall ![1, 0] ‖![1, 0]‖)

Points with positive first coordinate lie in the cone over the closed ball centered at ![1, 0].

theorem closure_cone_closedBall_has_point : ![0, 1] ∈ closure (convexConeGenerated 2 (Metric.closedBall ![1, 0] ‖![1, 0]‖))

The point (0, 1) lies in the closure of the cone over the closed ball centered at ![1, 0].

theorem counterexample_origin_boundary_or_unbounded_line : (∃ (n : ℕ) (x0 : Fin n → ℝ) (r : ℝ), have C := Metric.closedBall x0 r; 0 ∈ Metric.sphere x0 r ∧ IsClosed C ∧ Convex ℝ C ∧ True) ∧ ∃ (n : ℕ) (x0 : Fin n → ℝ) (v : Fin n → ℝ), have C := {x : Fin n → ℝ | ∃ (t : ℝ), x = x0 + t • v}; 0 ∉ C ∧ IsClosed C ∧ Convex ℝ C ∧ ¬Bornology.IsBounded C ∧ ¬IsClosed (convexConeGenerated n C)

Remark 9.6.1.2. The need for the condition 0 ∉ C in Theorem 9.6 and Corollary 9.6.1 is shown by the case where C is a closed ball with the origin on its boundary. The need for the boundedness assumption in Corollary 9.6.1 is shown by the case where C is a line not passing through the origin.

def prodLinearEquiv_append_coord (n : ℕ) : ((Fin n → ℝ) × ℝ) ≃ₗ[ℝ] Fin (n + 1) → ℝ

Coordinate version of prodLinearEquiv_append landing in Fin (n + 1) → Real.

Equations

• prodLinearEquiv_append_coord n = prodLinearEquiv_append.trans (EuclideanSpace.equiv (Fin (n + 1)) ℝ).toLinearEquiv

theorem epigraph_rightScalarMultiple_eq_smul {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {lam : ℝ} (hlam : 0 < lam) : epigraph Set.univ (rightScalarMultiple f lam) = (fun (p : (Fin n → ℝ) × ℝ) => lam • p) '' epigraph Set.univ f

The epigraph of a positive right scalar multiple is the scaled epigraph.

theorem smul_embedded_epigraph_eq_embedded_epigraph_rightScalarMultiple {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {lam : ℝ} (hlam : 0 < lam) : lam • ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f = ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ (rightScalarMultiple f lam)

Scaling the embedded epigraph corresponds to the right scalar multiple.

theorem closure_convexConeGenerated_embedded_epigraph_eq_union {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (hrec : (epigraph Set.univ f).recessionCone = epigraph Set.univ f0_plus) (hCne : (⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f).Nonempty) (hCclosed : IsClosed (⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f)) (hCconv : Convex ℝ (⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f)) (hC0 : 0 ∉ ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f) : have C := ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f; closure (convexConeGenerated (n + 1) C) = (⋃ (lam : ℝ), ⋃ (_ : 0 < lam), ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ (rightScalarMultiple f lam)) ∪ ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f0_plus

The closure of the cone over the embedded epigraph is the union of embedded right-scalar multiples and the embedded recession epigraph.

theorem convexConeGenerated_embedded_epigraph_eq_image_convexConeGeneratedEpigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) : have C := ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f; ⇑(prodLinearEquiv_append_coord n) '' convexConeGeneratedEpigraph f = convexConeGenerated (n + 1) C

The embedded image of the generated epigraph cone equals the generated cone of the embedded epigraph.

theorem convexConeGeneratedEpigraph_subset_epigraph_posHom {n : ℕ} {f : (Fin n → ℝ) → EReal} : have k := positivelyHomogeneousConvexFunctionGenerated f; convexConeGeneratedEpigraph f ⊆ epigraph Set.univ k

The generated epigraph cone lies in the epigraph of its inf-section.

theorem closure_convexConeGeneratedEpigraph_eq_union {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} (hclosure_union' : closure (⇑(prodLinearEquiv_append_coord n) '' convexConeGeneratedEpigraph f) = (⋃ (lam : ℝ), ⋃ (_ : 0 < lam), ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ (rightScalarMultiple f lam)) ∪ ⇑(prodLinearEquiv_append_coord n) '' epigraph Set.univ f0_plus) : closure (convexConeGeneratedEpigraph f) = (⋃ (lam : ℝ), ⋃ (_ : 0 < lam), epigraph Set.univ (rightScalarMultiple f lam)) ∪ epigraph Set.univ f0_plus

Remove the prodLinearEquiv_append_coord embedding from the closure/union formula.

theorem posHomGenerated_convex_and_nonempty {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfconv : ConvexFunctionOn Set.univ f) : have k := positivelyHomogeneousConvexFunctionGenerated f; ConvexFunctionOn Set.univ k ∧ (epigraph Set.univ k).Nonempty

The positively homogeneous hull is convex and has a nonempty epigraph.

theorem posHomGenerated_formula_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} (hfconv : ConvexFunctionOn Set.univ f) (hfinite : ∃ (x : Fin n → ℝ), f x ≠ ⊤) (hdom0 : 0 ∈ effectiveDomain Set.univ f) : have k := positivelyHomogeneousConvexFunctionGenerated f; ∀ (x : Fin n → ℝ), k x = sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple f lam x}

If 0 lies in the effective domain, the positive-scaling infimum formula holds.

theorem no_neg_vertical_recession_epigraph {n : ℕ} {f : (Fin n → ℝ) → EReal} (hproper : ProperConvexFunctionOn Set.univ f) {μ : ℝ} (hμ : μ < 0) : (0, μ) ∉ (epigraph Set.univ f).recessionCone

A proper epigraph has no negative vertical recession direction.