TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Proofs.DirectedBackwardState

Coefficient and constant invariants for backward CROWN #

An absent coefficient represents zero. A present coefficient box must have the node's width and enclose its exact real coefficient vector. This convention makes repeated parent occurrences ordinary additions, including cancellation between the two parents of subtraction.

source
def NN.MLTheory.CROWN.Graph.DirectedBackward.RowEncloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (box : FlatBox α) (n : ℕ) (f : ℕ → ℝ) :
Prop

A box has the expected width and encloses a real coefficient at each valid coordinate.

Instances For
    source
    def NN.MLTheory.CROWN.Graph.DirectedBackward.CoefficientsEnclose {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dims : ℕ → ℕ) (table : Array (Option (FlatBox α))) (f : ℕ → ℕ → ℝ) :
    Prop

    The coefficient table encloses an exact real coefficient for every node.

    Instances For
      source
      def NN.MLTheory.CROWN.Graph.DirectedBackward.StateEncloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dims : ℕ → ℕ) (st : Internal.DirectedBackwardState α) (f : ℕ → ℕ → ℝ) (c : ℝ) :
      Prop

      Both coefficient intervals and the accumulated constant contain an exact objective.

      Instances For
        source
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.addCoeff_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {st : Internal.DirectedBackwardState α} {f : ℕ → ℕ → ℝ} {c : ℝ} (hstate : StateEncloses dims st f c) (pid : ℕ) (hp : pid < st.coeffs.size) (box : FlatBox α) (a : ℕ → ℝ) (hbox : RowEncloses box (dims pid) a) :
        StateEncloses dims (Internal.addDirectedCoeff st pid box) (fun (id i : ℕ) => if id = pid then f id i + a i else f id i) c ∧ (Internal.addDirectedCoeff st pid box).failed = st.failed ∧ (Internal.addDirectedCoeff st pid box).coeffs.size = st.coeffs.size

        Updating one coefficient row adds its exact contribution, even when the row was absent.

        source
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.addConstant_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {st : Internal.DirectedBackwardState α} {f : ℕ → ℕ → ℝ} {c : ℝ} (hstate : StateEncloses dims st f c) (lo hi : α) (d : ℝ) (hd : LawfulBoundOps.toReal lo ≤ d ∧ d ≤ LawfulBoundOps.toReal hi) :
        StateEncloses dims (Internal.addDirectedConstant st lo hi) f (c + d)

        Accumulating a constant interval preserves enclosure of the exact shifted constant.

        source
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.negateCoeff_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {box : FlatBox α} {n : ℕ} {a : ℕ → ℝ} (hbox : RowEncloses box n a) :
        RowEncloses (Internal.negateDirectedCoeff box) n fun (i : ℕ) => -a i

        Negating a coefficient exchanges the endpoints and encloses its exact additive inverse.

        source
        @[simp]
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.addCoeff_size {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (st : Internal.DirectedBackwardState α) (pid : ℕ) (box : FlatBox α) :
        (Internal.addDirectedCoeff st pid box).coeffs.size = st.coeffs.size

        Coefficient accumulation never changes the number of graph rows, even on failure.

        source
        @[simp]
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.consume_size {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (st : Internal.DirectedBackwardState α) (aB xB : FlatBox α) :
        (Internal.consumeDirectedObjective st aB xB).coeffs.size = st.coeffs.size

        Discharging a node only changes the constant or the failure flag.

        source
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.addCoeff_failed {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (st : Internal.DirectedBackwardState α) (pid : ℕ) (box : FlatBox α) (h : st.failed = true) :
        (Internal.addDirectedCoeff st pid box).failed = true

        A failed state remains failed while accumulating any later coefficient.

        source
        theorem NN.MLTheory.CROWN.Graph.DirectedBackward.initial_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dims : ℕ → ℕ) (size output : ℕ) (obj : FlatTensor α) (hdim : obj.n = dims output) :
        StateEncloses dims { coeffs := (Array.replicate size none).set! output (some (FlatBox.ofTensor obj.v)), cstLo := 0, cstHi := 0 } (fun (id i : ℕ) => if id = output then LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i]) else 0) 0

        The initial table encloses the output objective and zero at every other node.