Documentation

LeanMlir.Proofs.Float.FloatClose

FloatClose — the float tier's one closeness form, and how it composes #

On inputs within magnitude A, the float fF is within an error modulus L e of the real f (per coordinate, at input error e), and both outputs are within B, so the next layer's magnitude precondition holds. FloatClose.comp composes two (moduli compose, magnitudes thread), so a whole-net float certificate is .comp folded over the layer list. of_close builds one from a per-op *_close budget; relu, id and iterate are the generic instances. The per-op instances for the conv-net op set are in FloatComposeBridge.

source
def Proofs.FloatClose {m n : ℕ} (A B : ℝ) (f fF : Vec m → Vec n) (L : ℝ → ℝ) :
Prop

A-posteriori-magnitude, proved-error float closeness, built to compose. A bounds the inputs (both real va and float vt), B both outputs; L is the input-error → output-error modulus.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Proofs.FloatClose.comp {m n p : ℕ} {A B C : ℝ} {f fF : Vec m → Vec n} {g gF : Vec n → Vec p} {Lf Lg : ℝ → ℝ} (hf : FloatClose A B f fF Lf) (hg : FloatClose B C g gF Lg) :
    FloatClose A C (g ∘ f) (gF ∘ fF) (Lg ∘ Lf)

    Float-closeness composes — the whole-net certificate backbone. Magnitudes thread A → B → C, error moduli compose Lg ∘ Lf.

    source
    theorem Proofs.FloatClose.of_close {m n : ℕ} {A R E : ℝ} {f fF : Vec m → Vec n} {L : ℝ → ℝ} (hreal : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → ∀ (i : Fin n), |f v i| ≤ R) (hround : ∀ (v : Vec m), (∀ (k : Fin m), |v k| ≤ A) → ∀ (i : Fin n), |fF v i - f v i| ≤ E) (herr : ∀ (vt va : Vec m) (e : ℝ), (∀ (k : Fin m), |va k| ≤ A) → (∀ (k : Fin m), |vt k| ≤ A) → (∀ (k : Fin m), |vt k - va k| ≤ e) → ∀ (i : Fin n), |fF vt i - f va i| ≤ L e) :
    FloatClose A (R + E) f fF L

    The standard way to build a FloatClose instance. A real bound R on the box, a rounding bound E at an exactly-represented input, and the error modulus give FloatClose A (R + E): the float output is within E of the real one, so its magnitude is at most R + E. Every per-op instance below with a fresh-input rounding term is this.

    source
    theorem Proofs.floatClose_relu {n : ℕ} (A : ℝ) :
    FloatClose A A (relu n) (relu n) fun (e : ℝ) => e

    ReLU is FloatClose with modulus id — exact in float (real = float map), 1-Lipschitz on the inherited error, never grows magnitudes.

    source
    theorem Proofs.floatClose_id {m : ℕ} (A : ℝ) :
    FloatClose A A id id id

    The identity map is FloatClose (modulus id).

    source
    theorem Proofs.floatClose_iterate {m : ℕ} {A : ℝ} {f fF : Vec m → Vec m} {L : ℝ → ℝ} (hf : FloatClose A A f fF L) (n : ℕ) :
    FloatClose A A f^[n] fF^[n] L^[n]

    THE FINAL FOLD: a magnitude-stable block iterated n times is FloatClose. A dim-preserving block that is FloatClose A A f fF L (its activations stay within the a-posteriori bound A — BN keeps them O(1), as the probe confirms) composes with itself to any depth: f^[n] is FloatClose A A with modulus L^[n]. This is r34's within-stage depth (n = 3,4,6,3); the whole net is these iterates .comp-joined with the stem / downsamples / GAP / dense. The depth-generic whole-net certificate — no per-depth re-proof.