Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Recession directions and no-line facts for subgradient sets

This module contains the recession-direction computations used to match Rockafellar's observation that interior-point subdifferentials contain no affine lines.

theorem AleksandrovDifferentiability.lineDirectionsAt.subset_recessionDirectionsAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {p : E} : lineDirectionsAt s p ⊆ recessionDirectionsAt s p

A line direction is in particular a recession direction.

theorem AleksandrovDifferentiability.ExposesPoint.inner_recessionDirection_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p q : E} (hexposed : ExposesPoint s normal p) (hqrec : q ∈ recessionDirectionsAt s p) (hq_ne : q ≠ 0) : inner ℝ normal q < 0

A nonzero recession direction at an exposed point pairs strictly negatively with the exposing normal.

theorem AleksandrovDifferentiability.ExposesPoint.inner_recessionDirection_nonpos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {normal p q : E} (hexposed : ExposesPoint s normal p) (hqrec : q ∈ recessionDirectionsAt s p) : inner ℝ normal q ≤ 0

Any recession direction at an exposed point pairs nonpositively with the exposing normal.

theorem AleksandrovDifferentiability.slope_nonpos_of_forall_nonneg_add_mul_le {a b c : ℝ} (h : ∀ (t : ℝ), 0 ≤ t → a + t * b ≤ c) : b ≤ 0

If a + t*b ≤ c for every nonnegative t, then b ≤ 0.

theorem AleksandrovDifferentiability.inner_recessionDirection_subgradientSet_nonpos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p q z : E} (_hp : SubgradientOn domain u y p) (hqrec : q ∈ recessionDirectionsAt {r : E | SubgradientOn domain u y r} p) (hz : z ∈ domain) : inner ℝ q (z - y) ≤ 0

A recession direction of the subdifferential gives a normal-cone inequality for the domain.

This is the local real-valued version of the Rockafellar 25.6 step identifying the recession cone of ∂f(y) with the normal cone to the effective domain at y.

theorem AleksandrovDifferentiability.recessionDirection_subgradientSet_of_forall_inner_sub_nonpos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p q : E} (hp : SubgradientOn domain u y p) (hnormal : ∀ z ∈ domain, inner ℝ q (z - y) ≤ 0) : q ∈ recessionDirectionsAt {r : E | SubgradientOn domain u y r} p

A normal-cone inequality for the domain gives a recession direction of the subdifferential.

This is the reverse implication in the local real-valued form of Rockafellar's identification K(y) = rec (∂u(y)).

theorem AleksandrovDifferentiability.recessionDirection_subgradientSet_iff_forall_inner_sub_nonpos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p q : E} (hp : SubgradientOn domain u y p) : q ∈ recessionDirectionsAt {r : E | SubgradientOn domain u y r} p ↔ ∀ z ∈ domain, inner ℝ q (z - y) ≤ 0

Recession directions of a subdifferential are exactly the domain normal-cone directions.

This packages the finite-valued local quantifier shape needed from Rockafellar 25.6.

theorem AleksandrovDifferentiability.eq_zero_of_forall_inner_sub_nonpos_of_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {y q : E} (hdomain : domain ∈ nhds y) (hnormal : ∀ z ∈ domain, inner ℝ q (z - y) ≤ 0) : q = 0

If the domain is a neighborhood of the base point, every normal-cone direction is zero.

theorem AleksandrovDifferentiability.recessionDirection_subgradientSet_eq_zero_of_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p q : E} (hdomain : domain ∈ nhds y) (hp : SubgradientOn domain u y p) (hqrec : q ∈ recessionDirectionsAt {r : E | SubgradientOn domain u y r} p) : q = 0

At an interior point of the domain, the subdifferential has no nonzero recession direction.

theorem AleksandrovDifferentiability.recessionDirectionsAt_subgradientSet_eq_singleton_zero_of_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p : E} (hdomain : domain ∈ nhds y) (hp : SubgradientOn domain u y p) : recessionDirectionsAt {r : E | SubgradientOn domain u y r} p = {0}

At an interior point of the domain, the based recession directions of the subdifferential are only the zero direction.

theorem AleksandrovDifferentiability.lineDirection_subgradientSet_eq_zero_of_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p q : E} (hdomain : domain ∈ nhds y) (hp : SubgradientOn domain u y p) (hqline : q ∈ lineDirectionsAt {r : E | SubgradientOn domain u y r} p) : q = 0

At an interior point of the domain, the subdifferential contains no nonzero affine line through a subgradient.

theorem AleksandrovDifferentiability.lineDirectionsAt_subgradientSet_eq_singleton_zero_of_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y p : E} (hdomain : domain ∈ nhds y) (hp : SubgradientOn domain u y p) : lineDirectionsAt {r : E | SubgradientOn domain u y r} p = {0}

At an interior point of the domain, the based affine-line directions in the subdifferential are only the zero direction. This is the local Lean form of Rockafellar's no-lines observation.

theorem AleksandrovDifferentiability.subgradientSet_hasNoAffineLines_of_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y : E} (hdomain : domain ∈ nhds y) : HasNoAffineLines {r : E | SubgradientOn domain u y r}

At an interior point of the domain, the subdifferential contains no nontrivial affine line.

theorem AleksandrovDifferentiability.subgradientSet_hasNoAffineLines_of_isOpen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {u : E → ℝ} {y : E} (hopen : IsOpen domain) : HasNoAffineLines {r : E | SubgradientOn domain u y r}

Open-domain version of subgradientSet_hasNoAffineLines_of_mem_nhds.