Tensor coordinates for normalization transfers #
The graph stores flat coordinate functions. These lemmas pass between those functions, read as
realTensor, and the typed tensors used by the real normalization specifications.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.rowEncloses_flatten_iff
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{s : Spec.Shape}
{lo hi : TorchLean.Tensor α s}
{f : ℕ → ℝ}
:
RowEncloses { dim := s.size, lo := lo.flattenSpec, hi := hi.flattenSpec } s.size f ↔ ∀ (c : s.Coord),
LawfulBoundOps.toReal (TorchLean.Tensor.Internal.Rep.get lo c) ≤ f ↑c.linearize ∧ f ↑c.linearize ≤ LawfulBoundOps.toReal (TorchLean.Tensor.Internal.Rep.get hi c)
A flattened box encloses a flat graph value exactly when it does so at every tensor coordinate.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.rowEncloses_unflatten
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{s : Spec.Shape}
{B : FlatBox α}
{f : ℕ → ℝ}
(h : RowEncloses B s.size f)
(c : s.Coord)
:
A flat parent enclosure supplies the coordinates of every checked tensor view. This is the
coordinatewise form of tensorEncloses_ibpUnflatten.