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

Basic Rockafellar-style subgradient cluster-density interfaces

This module contains the local cluster-density predicate, elementary topological wrappers for the Rockafellar ray construction, and the basic convex-gradient cluster facts used by later modules.

def AleksandrovDifferentiability.differentiabilitySetOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) : Set E

Differentiability points inside a prescribed sampling region.

Equations

• AleksandrovDifferentiability.differentiabilitySetOn s u = s ∩ {x : E | DifferentiableAt ℝ u x}

def AleksandrovDifferentiability.LocalSubgradientClusterDensityOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (domain sample : Set E) (u : E → ℝ) : Prop

Local interior form of the Rockafellar subgradient cluster-density conclusion.

For every point y in the sampling region and every subgradient p of u at y relative to the larger domain, p belongs to the closed convex hull of all ambient cluster values of gradient u along differentiability points in the sampling region approaching y.

The assumptions that the sets are open, convex, and nested are kept in the theorem statement below rather than inside this conclusion predicate.

Equations

• One or more equations did not get rendered due to their size.

theorem AleksandrovDifferentiability.mem_closure_convexHull_gradientClusterSet_of_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y p : E} (hdomain : domain ∈ nhds y) (hy : y ∈ sample) (hdu : DifferentiableAt ℝ u y) (hp : SubgradientOn domain u y p) : p ∈ closure ((convexHull ℝ) (HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y))

At a differentiability point, the local cluster-density conclusion is immediate.

Indeed, any subgradient relative to a neighborhood domain is the gradient, and that gradient is itself a cluster value through the non-punctured differentiability filter.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_forall_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} (hdomain : ∀ ⦃y : E⦄, y ∈ sample → domain ∈ nhds y) (hdu : ∀ ⦃y : E⦄, y ∈ sample → DifferentiableAt ℝ u y) : LocalSubgradientClusterDensityOn domain sample u

If u is differentiable on the whole sampling set and the domain is a neighborhood of each sample point, then the local cluster-density conclusion holds on that sampling set.

theorem AleksandrovDifferentiability.localSubgradientClusterDensityOn_of_isOpen_of_forall_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} (hopen : IsOpen domain) (hsubset : sample ⊆ domain) (hdu : ∀ ⦃y : E⦄, y ∈ sample → DifferentiableAt ℝ u y) : LocalSubgradientClusterDensityOn domain sample u

Open-domain version of localSubgradientClusterDensityOn_of_forall_differentiableAt.

theorem AleksandrovDifferentiability.IsOpen.exists_pos_forall_pos_lt_add_smul_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {domain : Set E} {y normal : E} (hopen : IsOpen domain) (hy : y ∈ domain) : ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃t : ℝ⦄, 0 < t → t < δ → y + t • normal ∈ domain

In an open domain, sufficiently small positive steps in any fixed direction remain in the domain.

This is the local interior replacement for the half-line/interior step in Rockafellar 25.6. In the global closed-function proof, one must show that the exposing half-line meets int (dom f). In the local source-cube theorem, the base point is already in an open domain, so openness gives the needed small positive ray directly.

theorem AleksandrovDifferentiability.tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_mem {E : Type u_1} [NormedAddCommGroup E] {ι : Type u_2} {l : Filter ι} {D : Set E} {φ : ι → E} {y : E} (hφ : Filter.Tendsto φ l (nhds y)) (hmem : ∀ᶠ (a : ι) in l, φ a ∈ D) : Filter.Tendsto φ l (nhdsWithin y D)

A map tending to y and eventually lying in D tends to y through D.

This small wrapper records the filter shape of the differentiability sequence in Rockafellar 25.6: after choosing differentiability points, the only remaining topological datum is ordinary convergence to the base point plus eventual membership in the differentiability set.

theorem AleksandrovDifferentiability.tendsto_add_smul_of_tendsto_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {ε : ι → ℝ} {y normal : E} (hε : Filter.Tendsto ε l (nhds 0)) : Filter.Tendsto (fun (a : ι) => y + ε a • normal) l (nhds y)

If the scalar parameter tends to zero, then the corresponding short ray tends to its base point.

This is the topological core of the sequence x_i ≈ y + ε_i • normal, ε_i → 0, used in the exposed-point argument of Rockafellar 25.6.

theorem AleksandrovDifferentiability.tendsto_nhdsWithin_of_tendsto_norm_sub_ray_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {D : Set E} {φ : ι → E} {ε : ι → ℝ} {y normal : E} (hε : Filter.Tendsto ε l (nhds 0)) (hmem : ∀ᶠ (a : ι) in l, φ a ∈ D) (hclose : Filter.Tendsto (fun (a : ι) => ‖φ a - (y + ε a • normal)‖) l (nhds 0)) : Filter.Tendsto φ l (nhdsWithin y D)

Rockafellar's ray-approach sequence tends to the base point through the chosen set.

The intended use is: D is the differentiability set, φ i is a differentiability point chosen near y + ε i • normal, ε i → 0, and the error norm tends to zero. The conclusion is exactly the approach-filter hypothesis needed by the directional exposed-subgradient cluster bridge.

theorem AleksandrovDifferentiability.tendsto_norm_sub_ray_zero_of_eventually_norm_sub_le_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {φ : ι → E} {ε : ι → ℝ} {y normal : E} (hε : Filter.Tendsto ε l (nhds 0)) (hclose : ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) : Filter.Tendsto (fun (a : ι) => ‖φ a - (y + ε a • normal)‖) l (nhds 0)

The explicit ε_i^2 closeness estimate in Rockafellar's construction forces the ray error to tend to zero.

theorem AleksandrovDifferentiability.tendsto_nhdsWithin_of_eventually_norm_sub_ray_le_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {D : Set E} {φ : ι → E} {ε : ι → ℝ} {y normal : E} (hε : Filter.Tendsto ε l (nhds 0)) (hmem : ∀ᶠ (a : ι) in l, φ a ∈ D) (hclose : ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) : Filter.Tendsto φ l (nhdsWithin y D)

Rockafellar's explicit ε_i^2 ray-approximation sequence tends to the base point through the chosen set.

theorem AleksandrovDifferentiability.unitDirection_pos_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (v : E) : ‖t • v‖⁻¹ • t • v = ‖v‖⁻¹ • v

Normalizing a positive scalar multiple does not change the unit direction.

theorem AleksandrovDifferentiability.tendsto_inv_smul_sub_ray_of_eventually_norm_sub_le_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {φ : ι → E} {ε : ι → ℝ} {y normal : E} (hε : Filter.Tendsto ε l (nhds 0)) (hεpos : ∀ᶠ (a : ι) in l, 0 < ε a) (hclose : ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) : Filter.Tendsto (fun (a : ι) => (ε a)⁻¹ • (φ a - (y + ε a • normal))) l (nhds 0)

The scaled error in Rockafellar's ε_i^2 ray approximation tends to zero.

If φ i is within ε_i^2 of y + ε_i • normal and ε_i > 0, then after rescaling by ε_i^{-1} the error is bounded by ε_i, hence tends to zero.

theorem AleksandrovDifferentiability.tendsto_unitDirection_sub_of_eventually_norm_sub_ray_le_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} {l : Filter ι} {φ : ι → E} {ε : ι → ℝ} {y normal : E} (hnormal : ‖normal‖ = 1) (hε : Filter.Tendsto ε l (nhds 0)) (hεpos : ∀ᶠ (a : ι) in l, 0 < ε a) (hclose : ∀ᶠ (a : ι) in l, ‖φ a - (y + ε a • normal)‖ ≤ ε a ^ 2) : Filter.Tendsto (fun (a : ι) => ‖φ a - y‖⁻¹ • (φ a - y)) l (nhds normal)

Rockafellar's explicit ray-approximation sequence approaches the exposing direction after normalization.

This formalizes the line in the source proof saying that from ||x_i - (x + ε_i y)|| < ε_i^2, ε_i ↓ 0, and ||y|| = 1, one gets (x_i - x) / ||x_i - x|| -> y. The statement is written with ≤ and filters, in the form used by the directional outer-semicontinuity bridge.

theorem AleksandrovDifferentiability.ConvexOn.subgradientOn_gradient_of_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain : Set E} {u : E → ℝ} {x : E} (hu : ConvexOn ℝ domain u) (hx : x ∈ interior domain) (hd : DifferentiableAt ℝ u x) : SubgradientOn domain u x (gradient u x)

At an interior differentiability point of a convex function, the gradient is a subgradient.

This is the finite-valued local version of the standard convex fact used in Rockafellar 25.6 at nearby differentiability points.

theorem AleksandrovDifferentiability.GradientClusterSet.subset_subgradientOn_of_convexOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {domain sample : Set E} {u : E → ℝ} {y q : E} (hu : ConvexOn ℝ domain u) (hsample : sample ⊆ interior domain) (hy : y ∈ sample) (hcont : ContinuousAt u y) (hq : q ∈ HasSubgradientLinearizationOnAt.GradientClusterSet (differentiabilitySetOn sample u) (gradient u) y) : SubgradientOn domain u y q

A gradient cluster value is a subgradient at the base point.

This packages the first closed-graph step in Rockafellar 25.6: gradients at nearby differentiability points are subgradients at those nearby points, and closedness of the subdifferential graph passes the supporting inequality to the cluster limit.

def AleksandrovDifferentiability.RockafellarLocalSubgradientClusterDensityStatement (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : Prop

The local theorem shape corresponding to the interior-point consequence of Rockafellar 25.6.

This is not an axiom; it is a named target for the remaining finite-dimensional convex-analysis work. In the source-cube application, domain = Q_3 and sample = Q_{3/2}.

Equations

• One or more equations did not get rendered due to their size.