Tensor enclosure for structural interval transfers

Coordinatewise enclosure is preserved by changes of shape, broadcasting, and directed axis summation. These lemmas use the tensor operations executed by the forward IBP dispatcher.

def NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} (lo hi : TorchLean.Tensor α s) (x : TorchLean.Tensor ℝ s) : Prop

A shaped endpoint pair encloses a real tensor at every coordinate.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.cast {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s t : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (hst : s = t) : TensorEncloses (hst ▸ lo) (hst ▸ hi) (hst ▸ x)

def NN.MLTheory.CROWN.Graph.DirectedBackward.realTensor (s : Spec.Shape) (f : ℕ → ℝ) : TorchLean.Tensor ℝ s

Reconstruct a real tensor from its row-major graph coordinates.

def NN.MLTheory.CROWN.Graph.DirectedBackward.tensorValues {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) (i : ℕ) : ℝ

Read the flat coordinates of a real tensor, extending them by zero out of bounds.

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.tensorValues_fin {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) (i : Fin s.size) : tensorValues x ↑i = x.flattenSpec.getScalar i

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.getScalar_flatten_realTensor (s : Spec.Shape) (f : ℕ → ℝ) (i : Fin s.size) : (realTensor s f).flattenSpec.getScalar i = f ↑i

@[simp]

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.realTensor_apply (s : Spec.Shape) (f : ℕ → ℝ) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (realTensor s f) c = f ↑c.linearize

realTensor reads the flat graph value at the row-major position of each coordinate.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.unstack {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} {s : Spec.Shape} {lo hi : TorchLean.Tensor α (Spec.Shape.dim n s)} {x : TorchLean.Tensor ℝ (Spec.Shape.dim n s)} (h : TensorEncloses lo hi x) (i : Fin n) : TensorEncloses (lo.unstack i) (hi.unstack i) (x.unstack i)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.dim {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} {s : Spec.Shape} {lo hi : Fin n → TorchLean.Tensor α s} {x : Fin n → TorchLean.Tensor ℝ s} (h : ∀ (i : Fin n), TensorEncloses (lo i) (hi i) (x i)) : TensorEncloses (TorchLean.Tensor.dim lo) (TorchLean.Tensor.dim hi) (TorchLean.Tensor.dim x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.reshape {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s t : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (hsize : TorchLean.Tensor.Internal.Shape.size s.toList = TorchLean.Tensor.Internal.Shape.size t.toList) : TensorEncloses (TorchLean.Tensor.Internal.Rep.reshape hsize lo) (TorchLean.Tensor.Internal.Rep.reshape hsize hi) (TorchLean.Tensor.Internal.Rep.reshape hsize x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.flatten {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) : TensorEncloses lo.flattenSpec hi.flattenSpec x.flattenSpec

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.unflatten {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α [s.size]} {x : TorchLean.Tensor ℝ [s.size]} (h : TensorEncloses lo hi x) : TensorEncloses (TorchLean.Tensor.unflattenSpec s lo) (TorchLean.Tensor.unflattenSpec s hi) (TorchLean.Tensor.unflattenSpec s x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.tensorEncloses_vector_iff {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} {lo hi : TorchLean.Tensor α [n]} {x : TorchLean.Tensor ℝ [n]} : TensorEncloses lo hi x ↔ ∀ (i : Fin n), LawfulBoundOps.toReal (lo.getScalar i) ≤ x.getScalar i ∧ x.getScalar i ≤ LawfulBoundOps.toReal (hi.getScalar i)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.tensorEncloses_ibpUnflatten {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {B : FlatBox α} {f : ℕ → ℝ} (hd : B.dim = s.size) (hB : RowEncloses B s.size f) : TensorEncloses (ibpUnflatten B.dim B.lo hd) (ibpUnflatten B.dim B.hi hd) (realTensor s f)

Flattened endpoint bounds recover enclosure of the shaped real input.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.row {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) {f : ℕ → ℝ} (hf : ∀ (i : Fin s.size), f ↑i = x.flattenSpec.getScalar i) : RowEncloses { dim := s.size, lo := lo.flattenSpec, hi := hi.flattenSpec } s.size f

A shaped enclosure gives the flat graph enclosure when the real coordinates agree.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.tensorValues {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) : RowEncloses { dim := s.size, lo := lo.flattenSpec, hi := hi.flattenSpec } s.size (DirectedBackward.tensorValues x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.getAtOrZero {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (indices : List ℕ) : LawfulBoundOps.toReal (Spec.getAtOrZero lo indices) ≤ Spec.getAtOrZero x indices ∧ Spec.getAtOrZero x indices ≤ LawfulBoundOps.toReal (Spec.getAtOrZero hi indices)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.broadcastPadded {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s t : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (k : ℕ) (hb : List.Forall₂ (fun (a b : ℕ) => a = b ∨ a = 1) (Spec.Shape.padLeft k s).toList t.toList) : TensorEncloses (TorchLean.Tensor.Broadcasting.Internal.broadcastPadded k hb lo) (TorchLean.Tensor.Broadcasting.Internal.broadcastPadded k hb hi) (TorchLean.Tensor.Broadcasting.Internal.broadcastPadded k hb x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.broadcastTo {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s t : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (hb : s.CanBroadcastTo t) : TensorEncloses (TorchLean.Tensor.broadcastTo hb lo) (TorchLean.Tensor.broadcastTo hb hi) (TorchLean.Tensor.broadcastTo hb x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.sum {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) : LawfulBoundOps.toReal (TorchLean.Tensor.foldlSpec BoundOps.addDown 0 lo) ≤ x.sumSpec ∧ x.sumSpec ≤ LawfulBoundOps.toReal (TorchLean.Tensor.foldlSpec BoundOps.addUp 0 hi)

A packed directed sum encloses the corresponding exact tensor sum.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.reduceOuterSum {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {n : ℕ} {lo hi : TorchLean.Tensor α (Spec.Shape.dim n s)} {x : TorchLean.Tensor ℝ (Spec.Shape.dim n s)} (h : TensorEncloses lo hi x) : TensorEncloses (TorchLean.Tensor.Reduction.Internal.reduceOuterAxis (fun {sliceShape : Spec.Shape} (row : TorchLean.Tensor α sliceShape) => TorchLean.Tensor.foldlSpec BoundOps.addDown 0 row) lo) (TorchLean.Tensor.Reduction.Internal.reduceOuterAxis (fun {sliceShape : Spec.Shape} (row : TorchLean.Tensor α sliceShape) => TorchLean.Tensor.foldlSpec BoundOps.addUp 0 row) hi) (TorchLean.Tensor.Reduction.Internal.reduceOuterAxis (fun {sliceShape : Spec.Shape} => TorchLean.Tensor.sumSpec) x)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.reduceSum {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (axis : ℕ) : TensorEncloses (TorchLean.Tensor.reduceDim (fun {sliceShape : Spec.Shape} (row : TorchLean.Tensor α sliceShape) => TorchLean.Tensor.foldlSpec BoundOps.addDown 0 row) axis lo) (TorchLean.Tensor.reduceDim (fun {sliceShape : Spec.Shape} (row : TorchLean.Tensor α sliceShape) => TorchLean.Tensor.foldlSpec BoundOps.addUp 0 row) axis hi) (TorchLean.Tensor.reduceDim (fun {sliceShape : Spec.Shape} => TorchLean.Tensor.sumSpec) axis x)

The induction follows both the selected axis and every surviving leading dimension.