Inexact-gradient descent over ℝ

The theorem that makes the FloatBridge budgets mean training, not just proximity: if the gradient oracle is within η of the true gradient and the loss is smooth along the step segment, the SGD step still decreases the loss — with an explicit decrease.

Shape, in suite style (everything coordinatewise over Vec, no inner-product spaces): gradAt f x i = fderiv ℝ f x (basisVec i) is the scalar-loss gradient entry — for the MLP loss these entries are exactly what the *_total_loss_grad / mlp_whole_net_weight_grads theorems certify, and the per-entry oracle error η is what FloatBridge's mulErr/cotErr budgets supply. The smoothness hypothesis is segment-local and coordinatewise (ℓ∞ on the gradient, ℓ1 on the displacement): for ReLU nets it is the descent-side cousin of the quantitative margins — the step segment must not cross a kink.

Proved via the one-dimensional mean value theorem on t ↦ f(x + t·d) — no integration; the price is the constant C·D² instead of the textbook C·D²/2, immaterial for a descent guarantee.

sgd_descends is the quotable form: if lr·η·‖∇f‖₁ ≤ lr·‖∇f‖₂²/4 and the curvature term is similarly dominated, one inexact step decreases the loss by at least lr·‖∇f‖₂²/2. Discharging its hypotheses for the concrete MNIST nets (actual Lipschitz constants for the MLP loss) is future work; this file is the ℝ-side keystone the float budgets plug into.

noncomputable def Proofs.gradAt {m : ℕ} (f : Vec m → ℝ) (x : Vec m) (i : Fin m) : ℝ

Gradient entry of a scalar loss: ∂f/∂xᵢ via the Mathlib fderiv — the scalar-codomain peer of pdiv.

Equations

• Proofs.gradAt f x i = (fderiv ℝ f x) (Proofs.basisVec i)

theorem Proofs.fderiv_apply_eq_sum_grad {m : ℕ} (f : Vec m → ℝ) (x d : Vec m) : (fderiv ℝ f x) d = ∑ i : Fin m, d i * gradAt f x i

Directional derivative = gradient contraction, coordinatewise.

theorem Proofs.descent_segment {m : ℕ} (f : Vec m → ℝ) (x d : Vec m) {C D : ℝ} (hC : 0 ≤ C) (hdiff : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ f (x + t • d)) (hD : ∑ j : Fin m, |d j| ≤ D) (hLip : ∀ t ∈ Set.Icc 0 1, ∀ (i : Fin m), |gradAt f (x + t • d) i - gradAt f x i| ≤ C * (t * D)) : f (x + d) ≤ f x + ∑ i : Fin m, d i * gradAt f x i + C * D ^ 2

Descent lemma along a segment (MVT form). If f is differentiable on the segment [x, x+d] and its gradient entries drift by at most C·(t·D) along it (D an ℓ1 bound on d), then f(x+d) ≤ f(x) + ⟨d, ∇f(x)⟩ + C·D².

theorem Proofs.sgd_descent_inexact {m : ℕ} (f : Vec m → ℝ) (x gh : Vec m) {lr η C : ℝ} (hlr : 0 ≤ lr) (hη : 0 ≤ η) (hC : 0 ≤ C) (hgh : ∀ (i : Fin m), |gh i - gradAt f x i| ≤ η) (hdiff : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ f (x + t • -(lr • gh))) (hLip : ∀ t ∈ Set.Icc 0 1, ∀ (i : Fin m), |gradAt f (x + t • -(lr • gh)) i - gradAt f x i| ≤ C * (t * (lr * (∑ j : Fin m, |gradAt f x j| + ↑m * η)))) : f (x - lr • gh) ≤ f x - lr * ∑ i : Fin m, gradAt f x i ^ 2 + lr * η * ∑ i : Fin m, |gradAt f x i| + C * (lr * (∑ j : Fin m, |gradAt f x j| + ↑m * η)) ^ 2

One inexact SGD step, explicit quadratic bound. With a gradient oracle gh within η of ∇f(x) coordinatewise, step x − lr·gh, and segment smoothness at the ℓ1 step radius lr·(‖∇f‖₁ + m·η):

f(x − lr·gh) ≤ f(x) − lr·‖∇f‖₂² + lr·η·‖∇f‖₁ + C·(lr·(‖∇f‖₁ + m·η))².

The three terms: full descent, the oracle-error tax, the curvature tax. FloatBridge supplies η (per-entry certified-gradient budgets); the smoothness hypothesis is the user's, segment-local — for ReLU nets it encodes that the step doesn't cross a kink.

theorem Proofs.sgd_descends {m : ℕ} (f : Vec m → ℝ) (x gh : Vec m) {lr η C : ℝ} (hlr : 0 ≤ lr) (hη : 0 ≤ η) (hC : 0 ≤ C) (hgh : ∀ (i : Fin m), |gh i - gradAt f x i| ≤ η) (hdiff : ∀ t ∈ Set.Icc 0 1, DifferentiableAt ℝ f (x + t • -(lr • gh))) (hLip : ∀ t ∈ Set.Icc 0 1, ∀ (i : Fin m), |gradAt f (x + t • -(lr • gh)) i - gradAt f x i| ≤ C * (t * (lr * (∑ j : Fin m, |gradAt f x j| + ↑m * η)))) (h1 : lr * η * ∑ i : Fin m, |gradAt f x i| ≤ (lr * ∑ i : Fin m, gradAt f x i ^ 2) / 4) (h2 : C * (lr * (∑ j : Fin m, |gradAt f x j| + ↑m * η)) ^ 2 ≤ (lr * ∑ i : Fin m, gradAt f x i ^ 2) / 4) : f (x - lr • gh) ≤ f x - (lr * ∑ i : Fin m, gradAt f x i ^ 2) / 2

Strict descent under explicit dominance. If the oracle-error tax and the curvature tax are each at most a quarter of the full descent, one inexact SGD step decreases the loss by at least lr·‖∇f‖₂²/2.