Directed broadcasting and axis reductions #
Successful transfers enclose the exact broadcast, sum, or mean. The runtime guards decide whether an axis is available; surviving axes may be empty. Mean denominators are bounded by the directed count fold, without assuming that a natural-number conversion is exact.
The exact sum along axis, in the runtime's flat output order.
Instances For
noncomputable def
NN.MLTheory.CROWN.Graph.DirectedBackward.realAxisMean
(s : Spec.Shape)
(axis : ℕ)
(f : ℕ → ℝ)
(i : ℕ)
:
The exact axis sum divided by the selected axis length.
Instances For
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpBroadcastTo_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{s t : Spec.Shape}
{B box : FlatBox α}
{f : ℕ → ℝ}
(hB : RowEncloses B s.size f)
(hb : s.CanBroadcastTo t)
(hbox : ibpBroadcastTo s t B = some box)
:
RowEncloses box t.size (tensorValues (TorchLean.Tensor.broadcastTo hb (realTensor s f)))
Broadcasting only selects coordinates of the input, at every valid rank and extent.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpBroadcastTo_canBroadcast
{α : Type}
[TorchLean.Storage α]
[Context α]
{s t : Spec.Shape}
{B box : FlatBox α}
(hbox : ibpBroadcastTo s t B = some box)
:
s.CanBroadcastTo t
A successful broadcast supplies its compatibility witness.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpReduceSumAxis_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{s : Spec.Shape}
{axis : ℕ}
{B box : FlatBox α}
{f : ℕ → ℝ}
(hB : RowEncloses B s.size f)
(hbox : ibpReduceSumAxis axis B s = some box)
:
RowEncloses box (TorchLean.Tensor.shapeAfterSum s axis).size (realAxisSum s axis f)
Directed summation encloses the exact sum over the selected axis.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.directed_count_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
(n : ℕ)
:
have count :=
List.foldl
(fun (x : α × α) (x_1 : ℕ) =>
match x with
| (lo, hi) => (BoundOps.addDown lo 1, BoundOps.addUp hi 1))
(0, 0) (List.range n);
LawfulBoundOps.toReal count.1 ≤ ↑n ∧ ↑n ≤ LawfulBoundOps.toReal count.2
The two directed counters enclose the exact natural length.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpReduceMeanAxis_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
[NonlinearBoundOps α]
[LawfulNonlinearBoundOps α]
{s : Spec.Shape}
{axis : ℕ}
{B box : FlatBox α}
{f : ℕ → ℝ}
(hB : RowEncloses B s.size f)
(hbox : ibpReduceMeanAxis axis B s = some box)
:
RowEncloses box (TorchLean.Tensor.shapeAfterSum s axis).size (realAxisMean s axis f)
Dividing each directed axis sum by an enclosing count encloses the exact axis mean.