Reference · Finite sums

rainbow.math.sums.bpath-walk

Finite sumssrc/rainbow/math/sums/bpath_walk.clj0 definitions, 8 theorems

Finite one-hot walks crossing a binary cut. Signed weights are unrestricted; the bottleneck aggregate is seeded by the first edge, never by zero.

Depends onmath.sums.bpath-cutmath.rational.signed.indexed-max-dominates

signed/binary-at-least-one-is-one :
  (bw-x : ℚ)
  (bw-bit : bw-x · (1 + signed/negate bw-x) = 0)
  (bw-lower : 1 ≤ bw-x)
  → bw-x = 1

signed/binary-at-most-zero-is-zero :
  (bw-x : ℚ)
  (bw-bit : bw-x · (1 + signed/negate bw-x) = 0)
  (bw-upper : bw-x ≤ 0)
  → bw-x = 0

signed/one-hot-walk-cut-bound-witness :
  (bw-Q bw-E : ℕ → ℕ → ℚ) (bw-S : ℕ → ℚ) (bw-W : ℕ → ℕ → ℚ) (bw-n bw-M : ℕ) (bw-b : ℚ)
  (bw-rows-binary : ∀ (bw-binary-row : ℕ), ∀ (bw-binary-row-bound : nat/strict-below bw-binary-row (data/succ bw-M)), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), (fun oh-v => bw-Q bw-binary-row oh-v) idx · (1 + signed/negate ((fun oh-v => bw-Q bw-binary-row oh-v) idx)) = 0)
  (bw-rows-unit : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ bw-M)), signed/expr-sum-value (fun oh-v => bw-Q idx oh-v) bw-n = 1)
  (bw-edges : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-M), (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (…⟨1⟩ …⟨1⟩) oh-v₁) oh-v · (fun oh-v₁ => bw-E oh-u oh-v₁) oh-v) bw-n) bw-n) idx = 1)
  (bw-cut-binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), bw-S idx · (1 + signed/negate (bw-S idx)) = 0)
  (bw-source : 1 ≤ signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q 0 oh-v₁) oh-v · bw-S oh-v) bw-n)
  (bw-sink : signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q bw-M oh-v₁) oh-v · bw-S oh-v) bw-n ≤ 0)
  (bw-cuts : ∀ (bc-u : ℕ), ∀ (bc-hu : nat/strict-below bc-u bw-n), ∀ (bc-v : ℕ), ∀ (bc-hv : nat/strict-below bc-v bw-n), bw-E bc-u bc-v · bw-S bc-u · ((1 + signed/negate (bw-S bc-v)) · (bw-b + signed/negate (bw-W bc-u bc-v))) ≤ 0)
  → proposition/existence ℕ (fun bw-hit => proposition/conjunction (nat/strict-below bw-hit bw-M) (bw-b ≤ (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => …⟨1⟩ …⟨3⟩ …⟨1⟩) oh-v · (fun oh-v₁ => …⟨1⟩ …⟨1⟩ …⟨1⟩) oh-v) bw-n) bw-n) bw-hit))

signed/indexed-max-from-upper-bound :
  (bw-F : ℕ → ℚ) (bw-init bw-R : ℚ) (bw-n : ℕ)
  (bw-init-upper : bw-init ≤ bw-R)
  (h₁ : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), bw-F idx ≤ bw-R)
  → signed/indexed-max-from bw-F bw-init bw-n ≤ bw-R

signed/indexed-max-lower-of-bound-witness :
  (bw-F : ℕ → ℚ) (bw-n : ℕ) (bw-b : ℚ)
  (bw-witness : proposition/existence ℕ (fun bw-hit => proposition/conjunction (nat/strict-below bw-hit bw-n) (bw-b ≤ bw-F bw-hit)))
  → bw-b ≤ signed/indexed-max-from bw-F (bw-F 0) bw-n

signed/indexed-max-attains-bound-of-witness :
  (bw-F : ℕ → ℚ) (bw-n : ℕ) (bw-b : ℚ)
  (bw-upper : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), bw-F idx ≤ bw-b)
  (bw-witness : proposition/existence ℕ (fun bw-hit => proposition/conjunction (nat/strict-below bw-hit bw-n) (bw-b ≤ bw-F bw-hit)))
  → signed/indexed-max-from bw-F (bw-F 0) bw-n = bw-b

signed/one-hot-walk-bottleneck-lower-bound :
  (bw-Q bw-E : ℕ → ℕ → ℚ) (bw-S : ℕ → ℚ) (bw-W : ℕ → ℕ → ℚ) (bw-n bw-M : ℕ) (bw-b : ℚ)
  (bw-rows-binary : ∀ (bw-binary-row : ℕ), ∀ (bw-binary-row-bound : nat/strict-below bw-binary-row (data/succ bw-M)), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), (fun oh-v => bw-Q bw-binary-row oh-v) idx · (1 + signed/negate ((fun oh-v => bw-Q bw-binary-row oh-v) idx)) = 0)
  (bw-rows-unit : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ bw-M)), signed/expr-sum-value (fun oh-v => bw-Q idx oh-v) bw-n = 1)
  (bw-edges : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-M), (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (…⟨1⟩ …⟨1⟩) oh-v₁) oh-v · (fun oh-v₁ => bw-E oh-u oh-v₁) oh-v) bw-n) bw-n) idx = 1)
  (bw-cut-binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), bw-S idx · (1 + signed/negate (bw-S idx)) = 0)
  (bw-source : 1 ≤ signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q 0 oh-v₁) oh-v · bw-S oh-v) bw-n)
  (bw-sink : signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q bw-M oh-v₁) oh-v · bw-S oh-v) bw-n ≤ 0)
  (bw-cuts : ∀ (bc-u : ℕ), ∀ (bc-hu : nat/strict-below bc-u bw-n), ∀ (bc-v : ℕ), ∀ (bc-hv : nat/strict-below bc-v bw-n), bw-E bc-u bc-v · bw-S bc-u · ((1 + signed/negate (bw-S bc-v)) · (bw-b + signed/negate (bw-W bc-u bc-v))) ≤ 0)
  → bw-b ≤ signed/indexed-max-from (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (data/succ bw-position) oh-v₁) oh-v · (fun oh-v₁ => bw-W oh-u oh-v₁) oh-v) bw-n) bw-n) ((fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (data/succ bw-position) oh-v₁) oh-v · (fun oh-v₁ => bw-W oh-u oh-v₁) oh-v) bw-n) bw-n) 0) bw-M

signed/one-hot-walk-bottleneck-attains :
  (bw-Q bw-E : ℕ → ℕ → ℚ) (bw-S : ℕ → ℚ) (bw-W : ℕ → ℕ → ℚ) (bw-n bw-M : ℕ) (bw-b : ℚ)
  (bw-rows-binary : ∀ (bw-binary-row : ℕ), ∀ (bw-binary-row-bound : nat/strict-below bw-binary-row (data/succ bw-M)), ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), (fun oh-v => bw-Q bw-binary-row oh-v) idx · (1 + signed/negate ((fun oh-v => bw-Q bw-binary-row oh-v) idx)) = 0)
  (bw-rows-unit : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ bw-M)), signed/expr-sum-value (fun oh-v => bw-Q idx oh-v) bw-n = 1)
  (bw-edges : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-M), (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (…⟨1⟩ …⟨1⟩) oh-v₁) oh-v · (fun oh-v₁ => bw-E oh-u oh-v₁) oh-v) bw-n) bw-n) idx = 1)
  (bw-cut-binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-n), bw-S idx · (1 + signed/negate (bw-S idx)) = 0)
  (bw-source : 1 ≤ signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q 0 oh-v₁) oh-v · bw-S oh-v) bw-n)
  (bw-sink : signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q bw-M oh-v₁) oh-v · bw-S oh-v) bw-n ≤ 0)
  (bw-cuts : ∀ (bc-u : ℕ), ∀ (bc-hu : nat/strict-below bc-u bw-n), ∀ (bc-v : ℕ), ∀ (bc-hv : nat/strict-below bc-v bw-n), bw-E bc-u bc-v · bw-S bc-u · ((1 + signed/negate (bw-S bc-v)) · (bw-b + signed/negate (bw-W bc-u bc-v))) ≤ 0)
  (bw-upper : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bw-M), (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (…⟨1⟩ …⟨1⟩) oh-v₁) oh-v · (fun oh-v₁ => bw-W oh-u oh-v₁) oh-v) bw-n) bw-n) idx ≤ bw-b)
  → signed/indexed-max-from (fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (data/succ bw-position) oh-v₁) oh-v · (fun oh-v₁ => bw-W oh-u oh-v₁) oh-v) bw-n) bw-n) ((fun bw-position => signed/expr-sum-value (fun oh-u => (fun oh-v => bw-Q bw-position oh-v) oh-u · signed/expr-sum-value (fun oh-v => (fun oh-v₁ => bw-Q (data/succ bw-position) oh-v₁) oh-v · (fun oh-v₁ => bw-W oh-u oh-v₁) oh-v) bw-n) bw-n) 0) bw-M = bw-b