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

Upper-contact line restriction consequences

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.subgradientOn_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {a : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : SubgradientOn s u x p

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.slope_unique_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p q : E} {a b : ℝ} (hp : HasUpperContactWithSlopeOn s u x p a) (hq : HasUpperContactWithSlopeOn s u x q b) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : p = q

Upper-contact slopes for a convex function at an interior point are unique.

theorem AleksandrovDifferentiability.HasUpperContactOn.exists_subgradient_contact_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a : ℝ} (h : HasUpperContactOn s u x a) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOn s u x p a

A convex upper quadratic contact at an interior point admits a slope which is simultaneously the contact slope and an ambient subgradient.

theorem AleksandrovDifferentiability.HasUpperContactOn.exists_subgradient_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a : ℝ} (h : HasUpperContactOn s u x a) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : ∃ (p : E), SubgradientOn s u x p

A convex upper quadratic contact at an interior point admits an ambient subgradient slope.

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.exists_subgradient_contact_add_pos_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A η : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hη : 0 < η) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOn s u x p (A + η)

A bounded upper-contact opening for a convex function gives, for every larger opening, a slope which is both a subgradient and an upper-contact slope.

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.exists_subgradient_fixedSlopeOpening_of_convex_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : ∃ (p : E), SubgradientOn s u x p ∧ HasUpperContactWithSlopeOpeningAtMostOn s u x p A

In the convex interior setting, an ordinary bounded upper-contact opening has a fixed slope: all larger openings can be realized with the same upper-contact slope.

theorem AleksandrovDifferentiability.SubgradientOn.directional_le_lineRightDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} (hp : SubgradientOn s u x p) (hu : ConvexOn ℝ s u) (h0 : 0 ∈ interior (lineDomain s x v)) : inner ℝ p v ≤ rightDeriv (lineRestriction u x v) 0

A subgradient controls the right derivative of every one-dimensional restriction.

theorem AleksandrovDifferentiability.SubgradientOn.directional_le_lineRightDeriv_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) : inner ℝ p v ≤ rightDeriv (lineRestriction u x v) t

A subgradient at an arbitrary point of a line controls the right derivative of the line restriction at the corresponding parameter.

theorem AleksandrovDifferentiability.SubgradientOn.lineLeftDeriv_le_directional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} (hp : SubgradientOn s u x p) (hu : ConvexOn ℝ s u) (h0 : 0 ∈ interior (lineDomain s x v)) : leftDeriv (lineRestriction u x v) 0 ≤ inner ℝ p v

A subgradient controls the left derivative of every one-dimensional restriction.

theorem AleksandrovDifferentiability.SubgradientOn.lineLeftDeriv_le_directional_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) : leftDeriv (lineRestriction u x v) t ≤ inner ℝ p v

A subgradient at an arbitrary point of a line controls the left derivative of the line restriction at the corresponding parameter.

theorem AleksandrovDifferentiability.SubgradientOn.directional_mem_Icc_leftDeriv_rightDeriv_at {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) : inner ℝ p v ∈ Set.Icc (leftDeriv (lineRestriction u x v) t) (rightDeriv (lineRestriction u x v) t)

At an interior line parameter, every ambient subgradient directional value lies in the one-dimensional subgradient interval of the line restriction.

theorem AleksandrovDifferentiability.SubgradientOn.directional_le_lineRightDeriv_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} (hp : SubgradientOn s u x p) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : inner ℝ p v ≤ rightDeriv (lineRestriction u x v) 0

Interior-domain version of the right-derivative bound along a line.

theorem AleksandrovDifferentiability.SubgradientOn.lineLeftDeriv_le_directional_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} (hp : SubgradientOn s u x p) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) : leftDeriv (lineRestriction u x v) 0 ≤ inner ℝ p v

Interior-domain version of the left-derivative bound along a line.

theorem AleksandrovDifferentiability.SubgradientOn.directional_le_lineRightDeriv_at_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) : inner ℝ p v ≤ rightDeriv (lineRestriction u x v) t

Interior-domain version of the arbitrary-parameter right-derivative bound along a line.

theorem AleksandrovDifferentiability.SubgradientOn.lineLeftDeriv_le_directional_at_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) : leftDeriv (lineRestriction u x v) t ≤ inner ℝ p v

Interior-domain version of the arbitrary-parameter left-derivative bound along a line.

theorem AleksandrovDifferentiability.SubgradientOn.directional_mem_Icc_leftDeriv_rightDeriv_at_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) : inner ℝ p v ∈ Set.Icc (leftDeriv (lineRestriction u x v) t) (rightDeriv (lineRestriction u x v) t)

Interior-domain version of the interval bound for ambient subgradient directional values.

theorem AleksandrovDifferentiability.SubgradientOn.exists_cluster_inner_ge_of_lineRightDeriv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s D : Set E} {u : E → ℝ} {G : E → E} {x p v : E} (hp : SubgradientOn s u x p) (hu : ConvexOn ℝ s u) (hx : x ∈ interior s) (hcluster : ∃ q ∈ HasSubgradientLinearizationOnAt.GradientClusterSet D G x, rightDeriv (lineRestriction u x v) 0 ≤ inner ℝ q v) : ∃ q ∈ HasSubgradientLinearizationOnAt.GradientClusterSet D G x, inner ℝ p v ≤ inner ℝ q v

If a cluster gradient dominates the right derivative of the line restriction, then it dominates every ambient subgradient in that direction.

theorem AleksandrovDifferentiability.eventually_directional_dominating_cluster_of_lineRightDeriv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s D approach : Set E} {u : E → ℝ} {G : E → E} {x : E} (hu : ConvexOn ℝ s u) (hinterior : ∀ᶠ (y : E) in nhdsWithin x approach, y ∈ interior s) (hcluster : ∀ᶠ (y : E) in nhdsWithin x approach, ∀ (v : E), ∃ q ∈ HasSubgradientLinearizationOnAt.GradientClusterSet D G y, rightDeriv (lineRestriction u y v) 0 ≤ inner ℝ q v) : ∀ᶠ (y : E) in nhdsWithin x approach, ∀ (p : E), SubgradientOn s u y p → ∀ (v : E), ∃ q ∈ HasSubgradientLinearizationOnAt.GradientClusterSet D G y, inner ℝ p v ≤ inner ℝ q v

Eventual version of the right-derivative-to-cluster bridge for all subgradients and directions.

theorem AleksandrovDifferentiability.SubgradientOn.lineRightDeriv_eq_inner_of_lineRightDeriv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) (hle : rightDeriv (lineRestriction u x v) t ≤ inner ℝ p v) : rightDeriv (lineRestriction u x v) t = inner ℝ p v

If a subgradient has directional value at least the right derivative, then it realizes the right derivative exactly. The reverse inequality is the general subgradient directional bound.

theorem AleksandrovDifferentiability.SubgradientOn.lineRightDeriv_eq_inner_of_lineRightDeriv_le_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) (hle : rightDeriv (lineRestriction u x v) t ≤ inner ℝ p v) : rightDeriv (lineRestriction u x v) t = inner ℝ p v

Interior-domain version of SubgradientOn.lineRightDeriv_eq_inner_of_lineRightDeriv_le.

theorem AleksandrovDifferentiability.SubgradientOn.lineLeftDeriv_eq_inner_of_inner_le_lineLeftDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : t ∈ interior (lineDomain s x v)) (hle : inner ℝ p v ≤ leftDeriv (lineRestriction u x v) t) : leftDeriv (lineRestriction u x v) t = inner ℝ p v

If a subgradient has directional value at most the left derivative, then it realizes the left derivative exactly. The reverse inequality is the general subgradient directional bound.

theorem AleksandrovDifferentiability.SubgradientOn.lineLeftDeriv_eq_inner_of_inner_le_lineLeftDeriv_of_mem_interior {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p v : E} {t : ℝ} (hp : SubgradientOn s u (x + t • v) p) (hu : ConvexOn ℝ s u) (ht : x + t • v ∈ interior s) (hle : inner ℝ p v ≤ leftDeriv (lineRestriction u x v) t) : leftDeriv (lineRestriction u x v) t = inner ℝ p v

Interior-domain version of SubgradientOn.lineLeftDeriv_eq_inner_of_inner_le_lineLeftDeriv.

theorem AleksandrovDifferentiability.ConvexOn.exists_subgradient_lineRightDeriv_eq_inner_of_isBounded_of_forall_isMaxOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [ProperSpace E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hne : {p : E | SubgradientOn s u (x + t • z) p}.Nonempty) (hb : Bornology.IsBounded {p : E | SubgradientOn s u (x + t • z) p}) (hmax_le : ∀ (p : E), SubgradientOn s u (x + t • z) p → IsMaxOn (fun (q : E) => inner ℝ q z) {q : E | SubgradientOn s u (x + t • z) q} p → rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t ≤ inner ℝ p z) : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ rightDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z

Compact-subdifferential right-endpoint attainment wrapper.

The hypothesis hmax_le is the support-function inequality expected from applying Mathlib's separation theorem to the epigraph/line-minorant configuration. The compactness and extreme-value boilerplate is handled here.

theorem AleksandrovDifferentiability.ConvexOn.exists_subgradient_lineLeftDeriv_eq_inner_of_isBounded_of_forall_isMinOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [ProperSpace E] {s : Set E} {u : E → ℝ} {x z : E} {t : ℝ} (hu : ConvexOn ℝ s u) (ht : x + t • z ∈ interior s) (hne : {p : E | SubgradientOn s u (x + t • z) p}.Nonempty) (hb : Bornology.IsBounded {p : E | SubgradientOn s u (x + t • z) p}) (hmin_le : ∀ (p : E), SubgradientOn s u (x + t • z) p → IsMinOn (fun (q : E) => inner ℝ q z) {q : E | SubgradientOn s u (x + t • z) q} p → inner ℝ p z ≤ leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t) : ∃ (p : E), SubgradientOn s u (x + t • z) p ∧ leftDeriv (AleksandrovDifferentiability.lineRestriction u x z) t = inner ℝ p z

Compact-subdifferential left-endpoint attainment wrapper.

The hypothesis hmin_le is the support-function inequality expected from applying Mathlib's separation theorem to the epigraph/line-minorant configuration.