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

Directional exposed-face outer semicontinuity

This module packages the subgradient inequalities and compactness wrapper leading to eventual membership in norm thickenings of an exposed face.

theorem AleksandrovDifferentiability.eventually_inner_le_unitDirection_of_subgradientOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {domain : Set E} {u : E → ℝ} {y r : E} {xs ps : ι → E} (hr : SubgradientOn domain u y r) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn domain u (xs i) (ps i)) : (fun (i : ι) => inner ℝ r (‖xs i - y‖⁻¹ • (xs i - y))) ≤ᶠ[l] fun (i : ι) => inner ℝ (ps i) (‖xs i - y‖⁻¹ • (xs i - y))

Directional monotonicity of subgradients from two supporting inequalities.

If r is a subgradient at y and ps i is a subgradient at xs i, then pairing both subgradient inequalities with the displacement xs i - y gives r · (xs i - y) ≤ ps i · (xs i - y). This is the elementary inequality behind Rockafellar's directional outer-semicontinuity theorem.

theorem AleksandrovDifferentiability.inner_le_of_subgradientOn_tendsto_direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} [l.NeBot] {domain : Set E} {u : E → ℝ} {y r q normal : E} {xs ps : ι → E} (hr : SubgradientOn domain u y r) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn domain u (xs i) (ps i)) (hdir : Filter.Tendsto (fun (i : ι) => ‖xs i - y‖⁻¹ • (xs i - y)) l (nhds normal)) (hps : Filter.Tendsto ps l (nhds q)) : inner ℝ normal r ≤ inner ℝ normal q

Directional closed-graph inequality for subgradients.

Let ps i ∈ ∂u(xs i) and suppose the normalized displacements ‖xs i - y‖⁻¹ • (xs i - y) tend to normal, while ps i tends to q. Then every base subgradient r ∈ ∂u(y) satisfies normal · r ≤ normal · q.

This is the Lean-local half-space form of the exposed-face conclusion in Rockafellar's directional outer-semicontinuity step.

theorem AleksandrovDifferentiability.tendsto_subgradientOn_mem_exposedFace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} [l.NeBot] {domain : Set E} {u : E → ℝ} {y q normal : E} {xs ps : ι → E} (hq : SubgradientOn domain u y q) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn domain u (xs i) (ps i)) (hdir : Filter.Tendsto (fun (i : ι) => ‖xs i - y‖⁻¹ • (xs i - y)) l (nhds normal)) (hps : Filter.Tendsto ps l (nhds q)) : q ∈ exposedFace {r : E | SubgradientOn domain u y r} normal

A convergent directional family of subgradients lands in the exposed face of the base subdifferential.

theorem AleksandrovDifferentiability.mapClusterPt_subgradientOn_mem_exposedFace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {domain : Set E} {u : E → ℝ} {y q normal : E} {xs ps : ι → E} (hq : SubgradientOn domain u y q) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn domain u (xs i) (ps i)) (hdir : Filter.Tendsto (fun (i : ι) => ‖xs i - y‖⁻¹ • (xs i - y)) l (nhds normal)) (hps : MapClusterPt q l ps) : q ∈ exposedFace {r : E | SubgradientOn domain u y r} normal

Cluster-point version of the directional exposed-face inequality for subgradients.

This is the form needed for the compactness upgrade in Rockafellar's directional outer-semicontinuity proof: ps need only have q as a cluster point, not as an ordinary limit.

theorem AleksandrovDifferentiability.IsCompact.eventually_mem_normThickening_exposedFace_of_directional_subgradientOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {domain : Set E} {u : E → ℝ} {y normal : E} {xs ps : ι → E} {K : Set E} (hK : IsCompact K) (hmemK : ∀ᶠ (i : ι) in l, ps i ∈ K) (hbase : ∀ q ∈ K, MapClusterPt q l ps → SubgradientOn domain u y q) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn domain u (xs i) (ps i)) (hdir : Filter.Tendsto (fun (i : ι) => ‖xs i - y‖⁻¹ • (xs i - y)) l (nhds normal)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ps i ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε

Compact directional outer-semicontinuity wrapper for moving subgradients.

If moving subgradients ps i ∈ ∂u(xs i) are eventually contained in a compact set K, every cluster point of ps inside K is a base subgradient at y, and the normalized directions from y to xs i tend to normal, then the moving subgradients are eventually in every positive norm-thickening of the exposed face of the base subdifferential.

theorem AleksandrovDifferentiability.IsCompact.eventually_mem_normThickening_exposedFace_of_directional_subgradientOn' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {domain : Set E} {u : E → ℝ} {y normal : E} {xs ps : ι → E} {K : Set E} (hK : IsCompact K) (hmemK : ∀ᶠ (i : ι) in l, ps i ∈ K) (hy : y ∈ domain) (hxs : Filter.Tendsto xs l (nhds y)) (hu : ContinuousAt u y) (hsub : ∀ᶠ (i : ι) in l, SubgradientOn domain u (xs i) (ps i)) (hdir : Filter.Tendsto (fun (i : ι) => ‖xs i - y‖⁻¹ • (xs i - y)) l (nhds normal)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ps i ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε

Compact directional outer-semicontinuity wrapper with the base-subgradient condition supplied by the local closed graph theorem.

This is the local finite-valued analogue of the compact part of Rockafellar's Theorem 24.6: cluster points of the moving subgradients become subgradients at the limit base point, and the directional inequality then puts them in the exposed face.

theorem AleksandrovDifferentiability.ConvexOn.eventually_gradient_mem_normThickening_exposedFace_of_compact_directional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ι : Type u_2} {l : Filter ι} {domain : Set E} {u : E → ℝ} {y normal : E} {φ : ι → E} {K : Set E} (huconv : ConvexOn ℝ domain u) (hK : IsCompact K) (hmemK : ∀ᶠ (i : ι) in l, gradient u (φ i) ∈ K) (hy : y ∈ domain) (hφ : Filter.Tendsto φ l (nhds y)) (hucont : ContinuousAt u y) (hφ_mem : ∀ᶠ (i : ι) in l, φ i ∈ interior domain) (hφ_diff : ∀ᶠ (i : ι) in l, DifferentiableAt ℝ u (φ i)) (hdir : Filter.Tendsto (fun (i : ι) => ‖φ i - y‖⁻¹ • (φ i - y)) l (nhds normal)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, gradient u (φ i) ∈ normThickening (exposedFace {q : E | SubgradientOn domain u y q} normal) ε

Gradient-sample form of the compact directional outer-semicontinuity wrapper.

At differentiability points of a convex function, gradient u is a subgradient. Therefore the moving-subgradient wrapper applies directly to differentiability samples approaching the base point in the exposing direction.