theorem wholeSpaceClarkePairDomain_eq_positiveTimes {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (d : E) : clarkeDirectionalDerivWithinDomain Set.univ d = {p : E × ℝ | 0 < p.2}

Helper for Chapter14 Lemma 14.1.1: in the whole-space specialization, the admissible Clarke pairs are exactly those with positive time component.

theorem wholeSpaceClarkePair_tendsto_shift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x e : E) : Filter.Tendsto (fun (p : E × ℝ) => (p.1 + p.2 • e, p.2)) (nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2}) (nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2})

Helper for Chapter14 Lemma 14.1.1: shifting the base point by t • e preserves the normalized whole-space Clarke pair filter.

theorem wholeSpaceClarkePair_tendsto_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {lam : ℝ} (h_lam : 0 < lam) : Filter.Tendsto (fun (p : E × ℝ) => (p.1, lam * p.2)) (nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2}) (nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2})

Helper for Chapter14 Lemma 14.1.1: rescaling the positive time variable by a positive scalar preserves the normalized whole-space Clarke pair filter.

theorem clarkeQuotient_add_eq_shifted_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (d₁ d₂ : E) (p : E × ℝ) (hp : 0 < p.2) : ↑((f (p.1 + p.2 • (d₁ + d₂)) - f p.1) / p.2) = ↑((f (p.1 + p.2 • d₂ + p.2 • d₁) - f (p.1 + p.2 • d₂)) / p.2) + ↑((f (p.1 + p.2 • d₂) - f p.1) / p.2)

Helper for Chapter14 Lemma 14.1.1: the Clarke quotient in direction d₁ + d₂ splits into the shifted d₁ quotient plus the d₂ quotient, matching the source decomposition for (14.1.9).

theorem clarkeQuotient_smul_eq_const_mul_rescaled {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (d : E) {lam : ℝ} (h_lam : 0 < lam) (p : E × ℝ) (hp : 0 < p.2) : ↑((f (p.1 + p.2 • lam • d) - f p.1) / p.2) = ↑lam * ↑((f (p.1 + (lam * p.2) • d) - f p.1) / (lam * p.2))

Helper for Chapter14 Lemma 14.1.1: on the positive-time Clarke-pair filter, the quotient in direction lam • d is the positive scalar lam times the quotient with rescaled time (y, t) ↦ (y, lam * t). This is the source pointwise algebra behind positive homogeneity.

theorem eventually_bounded_clarkeQuotient_of_locallyLipschitzAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x d : E) (h_local : LocallyLipschitzAt f x) : ∃ (K : NNReal), have l := nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2}; have q := fun (p : E × ℝ) => ↑((f (p.1 + p.2 • d) - f p.1) / p.2); (∀ᶠ (p : E × ℝ) in l, q p ≤ ↑(↑K * ‖d‖)) ∧ ∀ᶠ (p : E × ℝ) in l, ↑(-(↑K * ‖d‖)) ≤ q p

Helper for Chapter14 Lemma 14.1.1: a local Lipschitz witness gives one finite upper bound and one finite lower bound for the normalized whole-space Clarke quotient on the positive-time filter. This packages the boundedness side conditions that otherwise recur in every limsup transport.

theorem clarkeQuotient_limsup_rescale_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x d : E) (h_local : LocallyLipschitzAt f x) {lam : ℝ} (h_lam : 0 < lam) : have l := nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2}; have qr := fun (p : E × ℝ) => ↑((f (p.1 + (lam * p.2) • d) - f p.1) / (lam * p.2)); Filter.limsup qr l = clarkeDirectionalDeriv f x d

Helper for Chapter14 Lemma 14.1.1: positive rescaling of the time variable preserves the whole-space Clarke quotient limsup. This is the filter-transport bridge used in the 0 < lam branch of positive homogeneity.

theorem clarkeQuotient_limsup_shift_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x d e : E) (h_local : LocallyLipschitzAt f x) : have l := nhdsWithin (x, 0) {p : E × ℝ | 0 < p.2}; have q := fun (p : E × ℝ) => ↑((f (p.1 + p.2 • d) - f p.1) / p.2); Filter.limsup (fun (p : E × ℝ) => q (p.1 + p.2 • e, p.2)) l ≤ clarkeDirectionalDeriv f x d

Helper for Chapter14 Lemma 14.1.1: the source substitution y ↦ y + t • e transports the whole-space Clarke quotient in direction d back into the same positive-time filter, so the resulting limsup is bounded above by fᵒ(x; d).

theorem clarkeQuotient_neg_eq_negf_after_shift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (d : E) (p : E × ℝ) (_hp : 0 < p.2) : ↑((f (p.1 + p.2 • -d) - f p.1) / p.2) = ↑(((fun (y : E) => -f y) (p.1 + p.2 • -d + p.2 • d) - (fun (y : E) => -f y) (p.1 + p.2 • -d)) / p.2)

Helper for Chapter14 Lemma 14.1.1: after the source substitution u = y - t • d, the quotient in direction -d becomes the Clarke quotient of -f in direction d at the shifted base point.

theorem LocallyLipschitzAt.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (h_local : LocallyLipschitzAt f x) : LocallyLipschitzAt (fun (y : E) => -f y) x

Negating the target preserves local Lipschitz continuity at the same point.

theorem clarkeDirectionalDerivative_posHomogeneous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) (h_lipschitz : LocallyLipschitzAt f x) (d : E) (lam : ℝ) (h_lam : 0 ≤ lam) : clarkeDirectionalDeriv f x (lam • d) = ↑lam * clarkeDirectionalDeriv f x d

Chapter14 Lemma 14.1.1 (1): if f is Lipschitz near x, then its Clarke generalized directional derivative fᵒ(x; d) is positively homogeneous in the direction variable.

theorem clarkeDirectionalDerivative_subadditive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) (h_lipschitz : LocallyLipschitzAt f x) (d₁ d₂ : E) : clarkeDirectionalDeriv f x (d₁ + d₂) ≤ clarkeDirectionalDeriv f x d₁ + clarkeDirectionalDeriv f x d₂

Chapter14 Lemma 14.1.1 (2): if f is Lipschitz near x, then its Clarke generalized directional derivative fᵒ(x; d) is subadditive in the direction variable.

theorem clarkeQuotient_le_add_norm_sub_of_closedBallLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x y d d' : E) {t eps : ℝ} (ht : 0 < t) (K : NNReal) (hK : LipschitzOnWith K f (Metric.closedBall x eps)) (_hy : y ∈ Metric.closedBall x eps) (hyd : y + t • d ∈ Metric.closedBall x eps) (hyd' : y + t • d' ∈ Metric.closedBall x eps) : ↑((f (y + t • d') - f y) / t) ≤ ↑((f (y + t • d) - f y) / t) + ↑(↑K * ‖d' - d‖)

Helper for Chapter14 Lemma 14.1.1: on a fixed closed-ball Lipschitz neighborhood, the Clarke quotient in direction d' is bounded by the quotient in direction d plus K * ‖d' - d‖. This is the source inequality (14.1.10) before taking upper limits.

theorem clarkeDirectionalDerivative_abs_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x d : E) (K : NNReal) (h_lipschitz : ∃ (ε : ℝ), 0 < ε ∧ LipschitzOnWith K f (Metric.closedBall x ε)) : |clarkeDirectionalDerivReal f x d| ≤ ↑K * ‖d‖

Chapter14 Lemma 14.1.1 (3): if f is K-Lipschitz on some closed ball centered at x, then the absolute value of the finite real-valued Clarke directional derivative is bounded by K * ‖d‖.

theorem clarkeDirectionalDerivative_lipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) (h_lipschitz : LocallyLipschitzAt f x) : ∃ (K : NNReal), LipschitzWith K fun (d : E) => clarkeDirectionalDerivReal f x d

Chapter14 Lemma 14.1.1 (4): if f is Lipschitz near x, then the map sending d to the finite real-valued Clarke directional derivative is Lipschitz.

theorem clarkeQuotient_eventually_le_of_lt_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x d : E) {b : EReal} (hb : clarkeDirectionalDeriv f x d < b) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ {p : E × ℝ}, p ∈ Metric.closedBall (x, 0) ρ → 0 < p.2 → ↑((f (p.1 + p.2 • d) - f p.1) / p.2) ≤ b

Helper for Chapter14 Lemma 14.1.1: a strict upper bound on fᵒ(x; d) yields one closed-ball radius around ((x : E), 0) on which every positive-time quotient in direction d stays below the same cutoff. This packages the fixed-direction limsup bound into a witness-friendly metric statement.

theorem clarkeWitness_points_mem_closedBall_of_nearby_pair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x d : E) {eps : ℝ} (hε : 0 < eps) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ {x' d' : E} {p : E × ℝ}, (x', d') ∈ Metric.closedBall (x, d) ρ → p ∈ Metric.closedBall (x', 0) ρ → 0 < p.2 → p.1 ∈ Metric.closedBall x eps ∧ p.1 + p.2 • d ∈ Metric.closedBall x eps ∧ p.1 + p.2 • d' ∈ Metric.closedBall x eps

Helper for Chapter14 Lemma 14.1.1: one small product closed ball around (x, d) forces any positive-time Clarke witness based at a nearby (x', 0) to keep its base point and both directional endpoints inside the same closed ball around x. This is the geometric packaging needed before applying the fixed local Lipschitz witness.

theorem clarkeDirectionalDerivative_eventually_lt_coe_of_closedBallLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x d : E) {eps b : ℝ} (hε : 0 < eps) (K : NNReal) (hK : LipschitzOnWith K f (Metric.closedBall x eps)) (hb : clarkeDirectionalDeriv f x d < ↑b) : ∀ᶠ (p' : E × E) in nhds (x, d), clarkeDirectionalDeriv f p'.1 p'.2 < ↑b

Helper for Chapter14 Lemma 14.1.1: a fixed closed-ball Lipschitz witness around x turns any strict real cutoff for fᵒ(x; d) into an eventual strict real cutoff for nearby fᵒ(x'; d'). The proof keeps the source structure: freeze the d-quotient below an intermediate level c, then compare nearby quotients on the same positive-time witness.

theorem clarkeDirectionalDerivative_upperSemicontinuousAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) (h_lipschitz : LocallyLipschitzAt f x) (d : E) : UpperSemicontinuousAt (fun (p : E × E) => clarkeDirectionalDeriv f p.1 p.2) (x, d)

Chapter14 Lemma 14.1.1 (5): if f is Lipschitz near x, then (y, e) ↦ fᵒ(y; e) is upper semicontinuous at (x, d) on E × E.

theorem clarkeDirectionalDerivative_neg_direction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) (h_lipschitz : LocallyLipschitzAt f x) (d : E) : clarkeDirectionalDeriv f x (-d) = clarkeDirectionalDeriv (-f) x d

Chapter14 Lemma 14.1.1 (6): if f is Lipschitz near x, then the Clarke generalized directional derivative satisfies the sign-change identity fᵒ(x; -d) = (-f)ᵒ(x; d).