Documentation

LeanMlir.Proofs.Training.SgdDescent.Basic

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. The per-net discharges of the smoothness hypothesis (explicit segment-Lipschitz constants, one layer and one example at a time) are in SgdDescent.Linear, SgdDescent.Mlp and SgdDescent.Cnn; this file is the ℝ-side statement the float budgets plug into.

source
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
Instances For
    source
    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.

    source
    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².

    source
    noncomputable def Proofs.stepRadius {m : ℕ} (f : Vec m → ℝ) (x : Vec m) (lr η : ℝ) :
    ℝ

    The ℓ1 radius of an inexact SGD step on f at x: lr·(‖∇f(x)‖₁ + m·η), the right-hand side of sgd_step_l1_le at g := ∇f(x). Named so the descent capstones' margin hypotheses state it once instead of restating the gradient sum.

    Equations
    Instances For
      source
      theorem Proofs.sgd_step_l1_le {m : ℕ} (g gh : Vec m) {lr η : ℝ} (hlr : 0 ≤ lr) (hgh : ∀ (i : Fin m), |gh i - g i| ≤ η) :
      ∑ j : Fin m, |(-(lr • gh)) j| ≤ lr * (∑ j : Fin m, |g j| + ↑m * η)

      ℓ1 radius of an inexact SGD step. With the oracle gh within η of g coordinatewise, the step −lr·gh has ℓ1 mass at most lr·(‖g‖₁ + m·η) — the radius every descent capstone feeds descent_segment and its margin lemmas.

      source
      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.

      source
      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.