NF Tensor Approximation Plumbing

Shape-generic lemmas for approxT and linf_norm. The later NF proof files use these lemmas to turn scalar absolute-error facts into tensor-level forward-error bounds.

Tensor Approximation Plumbing

theorem Proofs.RuntimeApprox.linf_norm_nonneg {s : Spec.Shape} (t : Spec.SpecTensor s) : 0 ≤ linfNorm t

linf_norm is always nonnegative.

theorem Proofs.RuntimeApprox.linf_norm_le_get_dim {n : ℕ} {s : Spec.Shape} (t : Spec.SpecTensor (Spec.Shape.dim n s)) (i : Fin n) : linfNorm (match t with | Spec.Tensor.dim f => f i) ≤ linfNorm t

Componentwise bound for linf_norm on a dimensioned tensor.

The norm of any component t[i] is bounded by the norm of the whole tensor.

theorem Proofs.RuntimeApprox.approxT_scalar_iff {α : Type} {toSpec : α → Spec.SpecScalar} {x : Spec.SpecScalar} {xR : α} {eps : Spec.SpecScalar} : approxT toSpec (Spec.Tensor.scalar x) (Spec.Tensor.scalar xR) eps ↔ |toSpec xR - x| ≤ eps

Scalar characterization of approxT on scalar tensors.

This rewrites approxT (Tensor.scalar x) (Tensor.scalar xR) eps into the usual absolute-error inequality |toSpec xR - x| ≤ eps.

theorem Proofs.RuntimeApprox.approxT_dim_get {α : Type} {toSpec : α → Spec.SpecScalar} {n : ℕ} {s : Spec.Shape} {xS : Spec.SpecTensor (Spec.Shape.dim n s)} {xR : Spec.Tensor α (Spec.Shape.dim n s)} {eps : Spec.SpecScalar} (h : approxT toSpec xS xR eps) (i : Fin n) : approxT toSpec (match xS with | Spec.Tensor.dim f => f i) (match xR, h with | Spec.Tensor.dim f, h => f i) eps

Projection lemma for approxT on dimensioned tensors.

If xS approximates xR within eps, then each component xS[i] approximates xR[i] within eps.

theorem Proofs.RuntimeApprox.approxT_map_spec_of_scalar_bound {α : Type} {toSpec : α → Spec.SpecScalar} {s : Spec.Shape} (fS : Spec.SpecScalar → Spec.SpecScalar) (fR : α → α) (bnd : Spec.SpecScalar → Spec.SpecScalar → Spec.SpecScalar) {xS : Spec.SpecTensor s} {xR : Spec.Tensor α s} {eps : Spec.SpecScalar} : approxT toSpec xS xR eps → (∀ {x : Spec.SpecScalar} {xR : α}, |toSpec xR - x| ≤ eps → |toSpec (fR xR) - fS x| ≤ bnd (toSpec xR) eps) → approxT toSpec (Spec.Tensor.mapSpec fS xS) (Spec.Tensor.mapSpec fR xR) (linfNorm (Spec.Tensor.mapSpec (fun (a : Spec.SpecScalar) => bnd a eps) (tensorToSpec toSpec xR)))

Lift a scalar approximation bound to an elementwise map_spec.

Given a scalar bound of the form |toSpec (fR xR) - fS x| ≤ bnd (toSpec xR) eps and an input approximation approxT xS xR eps, this produces an approximation bound for map_spec fS xS vs map_spec fR xR, with an output epsilon computed by taking the linf_norm of the pointwise bound.

theorem Proofs.RuntimeApprox.approxT_map2_spec_of_scalar_bound {α : Type} {toSpec : α → Spec.SpecScalar} {s : Spec.Shape} (fS : Spec.SpecScalar → Spec.SpecScalar → Spec.SpecScalar) (fR : α → α → α) (bnd : Spec.SpecScalar → Spec.SpecScalar → Spec.SpecScalar → Spec.SpecScalar → Spec.SpecScalar) {xS yS : Spec.SpecTensor s} {xR yR : Spec.Tensor α s} {epsx epsy : Spec.SpecScalar} : approxT toSpec xS xR epsx → approxT toSpec yS yR epsy → (∀ {x y : Spec.SpecScalar} {xR yR : α}, |toSpec xR - x| ≤ epsx → |toSpec yR - y| ≤ epsy → |toSpec (fR xR yR) - fS x y| ≤ bnd (toSpec xR) (toSpec yR) epsx epsy) → approxT toSpec (Spec.Tensor.map2Spec fS xS yS) (Spec.Tensor.map2Spec fR xR yR) (linfNorm (Spec.Tensor.map2Spec (fun (a b : Spec.SpecScalar) => bnd a b epsx epsy) (tensorToSpec toSpec xR) (tensorToSpec toSpec yR)))

Lift a scalar approximation bound to an elementwise map2_spec.

This is the binary analogue of approxT_map_spec_of_scalar_bound, used for elementwise arithmetic (add, sub, mul_elem, etc.).