noncomputable def erealGradientErrorQuotient {n : ℕ} (f : (Fin n → ℝ) → EReal) (x g : Fin n → ℝ) : (Fin n → ℝ) → ℝ

The first-order error quotient for an EReal-valued function along finite-valued points.

noncomputable def HasERealGradientAt {n : ℕ} (f : (Fin n → ℝ) → EReal) (x g : Fin n → ℝ) : Prop

An EReal-valued function has gradient g at x when f x is finite and the normalized first-order error tends to 0 as z → x through finite-valued points of the punctured neighborhood of x.

noncomputable def ERealDifferentiableAt {n : ℕ} (f : (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : Prop

Definition 25.1: an EReal-valued function on ℝ^n is differentiable at x when there exists a vector g such that f x is finite and (f z - f x - g ⬝ᵥ (z - x)) / ‖z - x‖ → 0 as z → x through punctured nearby points where f is finite. In addition, nearby punctured points are eventually finite-valued, so the first-order expansion can be evaluated along every sufficiently short ray.

noncomputable def erealGradientAt {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hf : ERealDifferentiableAt f x) : Fin n → ℝ

A chosen gradient witness for an EReal-differentiable function at x.

theorem ERealDifferentiableAt.hasERealGradientAt {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hf : ERealDifferentiableAt f x) : HasERealGradientAt f x (erealGradientAt hf)

The chosen differentiability witness satisfies the first-order expansion predicate.

theorem ERealDifferentiableAt.finiteAt {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hf : ERealDifferentiableAt f x) : f x ≠ ⊤ ∧ f x ≠ ⊥

Differentiability at x forces f x to be finite.

theorem ERealDifferentiableAt.eventually_finiteValuedWithin_punctured {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hf : ERealDifferentiableAt f x) : ∀ᶠ (z : Fin n → ℝ) in nhdsWithin x {z : Fin n → ℝ | z ≠ x}, z ∈ effectiveDomain Set.univ f ∧ f z ≠ ⊥

Differentiability at x includes eventual finite-valued control on the punctured neighborhood of x.

theorem helperForTheorem_25_1_directionalDifferenceQuotient_tendsto_dotGradient_of_hasERealGradientAt {n : ℕ} {f : (Fin n → ℝ) → EReal} {x g y : Fin n → ℝ} (hg : HasERealGradientAt f x g) (hfinite : ∀ᶠ (z : Fin n → ℝ) in nhdsWithin x {z : Fin n → ℝ | z ≠ x}, z ∈ effectiveDomain Set.univ f ∧ f z ≠ ⊥) (hy : y ≠ 0) : Filter.Tendsto (directionalDifferenceQuotientAt f x y) (nhdsWithin 0 (Set.Ioi 0)) (nhds ↑(g ⬝ᵥ y))

Helper for Theorem 25.1: a gradient witness together with eventual finite-valued control identifies every nonzero directional difference quotient limit.

theorem erealGradient_unique {n : ℕ} {f : (Fin n → ℝ) → EReal} {x g₁ g₂ : Fin n → ℝ} (hfinite : ∀ᶠ (z : Fin n → ℝ) in nhdsWithin x {z : Fin n → ℝ | z ≠ x}, z ∈ effectiveDomain Set.univ f ∧ f z ≠ ⊥) (hg₁ : HasERealGradientAt f x g₁) (hg₂ : HasERealGradientAt f x g₂) : g₁ = g₂

Two gradients satisfying the first-order expansion at the same point coincide once nearby punctured points are eventually finite-valued.

theorem helperForTheorem_25_1_nonzero_ray_ne {n : ℕ} {x y : Fin n → ℝ} (hy : y ≠ 0) {t : ℝ} (ht : 0 < t) : x + t • y ≠ x

Helper for Theorem 25.1: a positive step in a nonzero direction never returns to the base point.

theorem helperForTheorem_25_1_tendsto_ray_to_puncturedNeighborhood {n : ℕ} {x y : Fin n → ℝ} (hy : y ≠ 0) : Filter.Tendsto (fun (t : ℝ) => x + t • y) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin x {z : Fin n → ℝ | z ≠ x})

Helper for Theorem 25.1: the positive ray t ↦ x + t • y tends to x through the punctured neighborhood whenever y ≠ 0.

theorem helperForTheorem_25_1_eventually_mem_puncturedEffectiveDomain_of_eventually_mem_effectiveDomain_ray {n : ℕ} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} (hy : y ≠ 0) (hray : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), x + t • y ∈ effectiveDomain Set.univ f) : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), x + t • y ∈ {z : Fin n → ℝ | z ≠ x} ∩ effectiveDomain Set.univ f

Helper for Theorem 25.1: eventual effective-domain membership along a positive ray upgrades to eventual membership in the punctured effective-domain filter used by HasERealGradientAt.

theorem helperForTheorem_25_1_tendsto_ray_to_puncturedEffectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} (hy : y ≠ 0) (hray : ∀ᶠ (t : ℝ) in nhdsWithin 0 (Set.Ioi 0), x + t • y ∈ effectiveDomain Set.univ f) : Filter.Tendsto (fun (t : ℝ) => x + t • y) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin x ({z : Fin n → ℝ | z ≠ x} ∩ effectiveDomain Set.univ f))

Helper for Theorem 25.1: under eventual finite-valued control on the ray, the ray map tends into the punctured effective-domain neighborhood of x.

theorem helperForTheorem_25_1_directionalDifferenceQuotient_tendsto_dotGradient {n : ℕ} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} (hf : ERealDifferentiableAt f x) (hy : y ≠ 0) : Filter.Tendsto (directionalDifferenceQuotientAt f x y) (nhdsWithin 0 (Set.Ioi 0)) (nhds ↑(erealGradientAt hf ⬝ᵥ y))

Helper for Theorem 25.1: differentiability identifies each nonzero directional difference quotient limit with the dot product against the chosen gradient witness.

theorem helperForTheorem_25_1_eq_of_dotProduct_eq {n : ℕ} {g₁ g₂ : Fin n → ℝ} (hdot : ∀ (y : Fin n → ℝ), g₁ ⬝ᵥ y = g₂ ⬝ᵥ y) : g₁ = g₂

Helper for Theorem 25.1: equality of all Euclidean pairings forces equality of the underlying vectors.

theorem helperForTheorem_25_1_gradient_gives_subgradient_and_directionalDerivative {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) {x : Fin n → ℝ} (hdiff : ERealDifferentiableAt f x) : (∀ (y : Fin n → ℝ), upperDirectionalDerivativeAt f x y = ↑(erealGradientAt hdiff ⬝ᵥ y)) ∧ IsSubgradientAt f x ((dotProductEquiv ℝ (Fin n)) (erealGradientAt hdiff))

Helper for Theorem 25.1: differentiability identifies the upper directional derivative with the gradient pairing, and therefore the chosen gradient is a Euclidean subgradient.

theorem helperForTheorem_25_1_uniqueSubgradient_implies_linearDirectionalDerivative {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunction f) {x : Fin n → ℝ} (hx : f x ≠ ⊤ ∧ f x ≠ ⊥) (huniq : ∃! g : Fin n → ℝ, IsSubgradientAt f x ((dotProductEquiv ℝ (Fin n)) g)) : ∃ (g : Fin n → ℝ), ProperConvexFunctionOn Set.univ f ∧ x ∈ interior (effectiveDomain Set.univ f) ∧ ∀ (y : Fin n → ℝ), upperDirectionalDerivativeAt f x y = ↑(g ⬝ᵥ y)

Helper for Theorem 25.1: a unique Euclidean subgradient already forces properness, interiority of the effective domain, and a linear directional derivative formula.

theorem helperForTheorem_25_1_exists_closedBall_subset_of_isOpen {n : ℕ} {C : Set (Fin n → ℝ)} (hCopen : IsOpen C) {x : Fin n → ℝ} (hx : x ∈ C) : ∃ (r : ℝ), 0 < r ∧ Metric.closedBall x r ⊆ C

Helper for Theorem 25.1: an open set containing x contains a smaller closed ball around x.

theorem helperForTheorem_25_1_subgradient_of_linearDirectionalDerivative {n : ℕ} {f : (Fin n → ℝ) → EReal} {x g : Fin n → ℝ} (hproper : ProperConvexFunctionOn Set.univ f) (hxInt : x ∈ interior (effectiveDomain Set.univ f)) (hdir : ∀ (y : Fin n → ℝ), upperDirectionalDerivativeAt f x y = ↑(g ⬝ᵥ y)) : IsSubgradientAt f x ((dotProductEquiv ℝ (Fin n)) g)

Helper for Theorem 25.1: linearity of the upper directional derivative identifies g as the Euclidean subgradient at x.

theorem helperForTheorem_25_1_exists_closedBall_subset_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hxInt : x ∈ interior (effectiveDomain Set.univ f)) : ∃ (ρ : ℝ), 0 < ρ ∧ Metric.closedBall x ρ ⊆ effectiveDomain Set.univ f

Helper for Theorem 25.1: interior-domain membership provides a closed ball that stays inside the effective domain.

theorem helperForTheorem_25_1_exists_closedBall_subset_interior_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hxInt : x ∈ interior (effectiveDomain Set.univ f)) : ∃ (ρ : ℝ), 0 < ρ ∧ Metric.closedBall x ρ ⊆ interior (effectiveDomain Set.univ f)

Helper for Theorem 25.1: interior-domain membership provides a closed ball that stays inside the interior of the effective domain.

theorem helperForTheorem_25_1_exists_closedBall_finiteValues {n : ℕ} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hproper : ProperConvexFunctionOn Set.univ f) (hxInt : x ∈ interior (effectiveDomain Set.univ f)) : ∃ (ρ : ℝ), 0 < ρ ∧ ∀ z ∈ Metric.closedBall x ρ, f z ≠ ⊤ ∧ f z ≠ ⊥

Helper for Theorem 25.1: on the closed ball supplied by interiority, all values of f are finite.

noncomputable def helperForTheorem_25_1_dyadicScale (ρ : ℝ) : ℕ → ℝ

Helper for Theorem 25.1: the dyadic scales used to compare arbitrary small secants with one fixed remainder function.

noncomputable def helperForTheorem_25_1_dyadicRemainder {n : ℕ} (f : (Fin n → ℝ) → EReal) (x g : Fin n → ℝ) (ρ : ℝ) : ℕ → (Fin n → ℝ) → ℝ

Helper for Theorem 25.1: the dyadic real-valued remainder family whose uniform convergence to zero would imply differentiability.

theorem helperForTheorem_25_1_dyadicScale_pos {ρ : ℝ} (hρpos : 0 < ρ) (i : ℕ) : 0 < helperForTheorem_25_1_dyadicScale ρ i

Helper for Theorem 25.1: every dyadic comparison scale is positive.

theorem helperForTheorem_25_1_dyadicScale_le_radius {ρ : ℝ} (hρpos : 0 < ρ) (i : ℕ) : helperForTheorem_25_1_dyadicScale ρ i ≤ ρ

Helper for Theorem 25.1: every dyadic comparison scale stays below the ambient finite-valued radius.

theorem helperForTheorem_25_1_dyadicScale_tendsto_zero {ρ : ℝ} : Filter.Tendsto (helperForTheorem_25_1_dyadicScale ρ) Filter.atTop (nhds 0)

Helper for Theorem 25.1: the dyadic scales approach zero along atTop.

theorem helperForTheorem_25_1_step_mem_closedBall_of_mem_closedUnitBall {n : ℕ} {x u : Fin n → ℝ} {ρ : ℝ} (hρpos : 0 < ρ) (i : ℕ) (hu : u ∈ Metric.closedBall 0 1) : x + helperForTheorem_25_1_dyadicScale ρ i • u ∈ Metric.closedBall x ρ

Helper for Theorem 25.1: directions in the closed unit ball stay inside the closed finite ball after one dyadic step.

theorem helperForTheorem_25_1_remainderSequence_continuousOn_closedUnitBall {n : ℕ} {f : (Fin n → ℝ) → EReal} {x g : Fin n → ℝ} {ρ : ℝ} (hproper : ProperConvexFunctionOn Set.univ f) (hxInt : x ∈ interior (effectiveDomain Set.univ f)) (hρpos : 0 < ρ) (hρsub : Metric.closedBall x ρ ⊆ interior (effectiveDomain Set.univ f)) (i : ℕ) : ContinuousOn (helperForTheorem_25_1_dyadicRemainder f x g ρ i) (Metric.closedBall 0 1)

Helper for Theorem 25.1: each dyadic remainder function is continuous on the closed unit ball once the comparison ball stays inside the interior of the effective domain.

theorem helperForTheorem_25_1_remainderSequence_antitone_nonneg_tendsto_zero {n : ℕ} {f : (Fin n → ℝ) → EReal} {x g u : Fin n → ℝ} {ρ : ℝ} (hf : ConvexFunction f) (hxFinite : f x ≠ ⊤ ∧ f x ≠ ⊥) (hρpos : 0 < ρ) (hfiniteStep : ∀ (i : ℕ), f (x + helperForTheorem_25_1_dyadicScale ρ i • u) ≠ ⊤ ∧ f (x + helperForTheorem_25_1_dyadicScale ρ i • u) ≠ ⊥) (hdiru : upperDirectionalDerivativeAt f x u = ↑(g ⬝ᵥ u)) (hsub : IsSubgradientAt f x ((dotProductEquiv ℝ (Fin n)) g)) : (Antitone fun (i : ℕ) => helperForTheorem_25_1_dyadicRemainder f x g ρ i u) ∧ (∀ (i : ℕ), 0 ≤ helperForTheorem_25_1_dyadicRemainder f x g ρ i u) ∧ Filter.Tendsto (fun (i : ℕ) => helperForTheorem_25_1_dyadicRemainder f x g ρ i u) Filter.atTop (nhds 0)

Helper for Theorem 25.1: for a fixed direction in the closed unit ball, the dyadic remainder sequence is antitone, nonnegative, and tends to 0.

theorem helperForTheorem_25_1_remainderSequence_tendstoUniformlyOn_closedUnitBall {n : ℕ} {f : (Fin n → ℝ) → EReal} {x g : Fin n → ℝ} {ρ : ℝ} (hproper : ProperConvexFunctionOn Set.univ f) (hxInt : x ∈ interior (effectiveDomain Set.univ f)) (hρpos : 0 < ρ) (hρsub : Metric.closedBall x ρ ⊆ interior (effectiveDomain Set.univ f)) (hdir : ∀ (y : Fin n → ℝ), upperDirectionalDerivativeAt f x y = ↑(g ⬝ᵥ y)) (hsub : IsSubgradientAt f x ((dotProductEquiv ℝ (Fin n)) g)) : TendstoUniformlyOn (helperForTheorem_25_1_dyadicRemainder f x g ρ) (fun (x : Fin n → ℝ) => 0) Filter.atTop (Metric.closedBall 0 1)

Helper for Theorem 25.1: Dini's theorem upgrades the dyadic remainder sequence to uniform convergence on the closed unit ball.