Reference · Finite sums

rainbow.math.sums.flow-cut

Finite sumssrc/rainbow/math/sums/flow_cut.clj0 definitions, 9 theorems

General lemmas: flow cut. The mathematical facts the corresponding checks rest on, each checked by the kernel.

Depends onmath.sums.value-appendmath.nat.infinitemath.rational.nnrat.identitiesmath.nat.at-most-cancellationmath.rational.nnrat.order-equivalencemath.rational.nnrat.archimedeanmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellationmath.rational.nnrat.additive-reassociationmath.rational.signed.order-transitivitymath.rational.signed.convergencemath.rational.signed.order-respectsmath.rational.signed.limit-uniquenessmath.rational.signed.strict-ordermath.rational.signed.multiplymath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.ringmath.rational.nnrat.multiply-monotonemath.rational.nnrat.order-differencemath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.rational.nnrat.minmaxmath.rational.nnrat.farkas-elim-listmath.rational.signed.no-zero-divisorsmath.rational.signed.decide-ordermath.rational.signed.decide-reflexivemath.logic.boolean-andmath.rational.signed.decide-equivalencemath.rational.signed.decide-completenessmath.rational.signed.unit-lawsmath.nat.strict-below-splitmath.nat.strict-below-moremath.checksmath.nat.at-most-addmath.rational.nnrat.harmonic-convergencemath.nat.divmodmath.rational.signed.minmaxmath.rational.signed.minmax-algebramath.rational.signed.clampmath.rational.signed.deviation-rowsmath.rational.signed.absolutemath.rational.signed.absolute-algebramath.rational.signed.distancemath.nat.linear-ordermath.rational.signed.add-associativemath.nat.semiringmath.nat.multiply-zero-splitmath.rational.nnrat.multiply-zero-splitmath.nat.monusmath.rational.nnrat.monusmath.rational.nnrat.add-zero-splitmath.rational.nnrat.add-cancel-zeromath.finite.rational-argmaxmath.rational.nnrat.order-totalmath.rational.nnrat.multiply-difference-zeromath.linear.vector.norm-nonnegativemath.linear.vector.norm-zero-reflectionalgorithms.proofs.counterfactual-distance-separationalgorithms.proofs.counterfactual-distance-lawsmath.finite.matrixmath.linear.matrix.equivalencemath.linear.matrix.transposemath.linear.matrix.transpose-equivalencemath.linear.matrix.multiplymath.linear.matrix.multiply-shapemath.linear.matrix.composablemath.linear.matrix.composable-multiplymath.linear.vector.additive-unitsmath.linear.vector.shape-cancellationmath.linear.vector.shape-mapmath.linear.vector.shape-addmath.linear.vector.dot-additivemath.linear.vector.dot-bilinearmath.linear.vector.dot-negatemath.linear.vector.dot-subtractmath.linear.vector.dot-scalemath.linear.matrix.action-scalemath.rational.signed.multiply-nonzeromath.rational.signed.order-monotonemath.rational.signed.list-summath.rational.signed.multiply-monotonemath.rational.signed.map-sum-algebramath.rational.signed.negate-additivemath.rational.signed.lp-objective-negatemath.nat.pair-index-inverse

signed/expr-sum-value-rectangular :
  (F : ℕ → ℚ) (n m : ℕ)
  → signed/expr-sum-value F (nat/multiply m n) = signed/expr-sum-value (fun i => signed/expr-sum-value (fun j => F (algebra/nat-add j (nat/multiply i n))) n) m

signed/expr-sum-value-head-tail :
  (F : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value F (data/succ n) = F 0 + signed/expr-sum-value (fun i => F (data/succ i)) n

signed/zero-one-of-boolean-polynomial :
  (x : ℚ)
  (boolean : x · (1 + signed/negate x) = 0)
  → proposition/disjunction (x = 0) (x = 1)

signed/expr-sum-value-subtract :
  (F G : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun i => F i + signed/negate (G i)) n = signed/expr-sum-value F n + signed/negate (signed/expr-sum-value G n)

signed/expr-sum-weighted-divergence :
  (F : ℕ → ℕ → ℚ) (S : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun i => S i · (signed/expr-sum-value (fun column-index => F i column-index) n + signed/negate (signed/expr-sum-value (fun row-index => F row-index i) n))) n = signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun i₁ => fun j => (S i₁ + signed/negate (S j)) · F i₁ j) i column-index) n) n

signed/expr-sum-conservation-boundary :
  (S D : ℕ → ℚ) (m : ℕ)
  (source : S 0 = 1)
  (sink : S (data/succ m) = 0)
  (internal : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), D (data/succ idx) = 0)
  → signed/expr-sum-value (fun i => S i · D i) (data/succ (data/succ m)) = D 0

signed/flow-cut-edge-bound :
  (a b flow capacity : ℚ)
  (a-bit : a · (1 + signed/negate a) = 0)
  (b-bit : b · (1 + signed/negate b) = 0)
  (nonnegative : 0 ≤ flow)
  (capacity-bound : flow ≤ capacity)
  → (a + signed/negate b) · flow ≤ a · (1 + signed/negate b) · capacity

signed/expr-sum-flow-cut-weak-duality :
  (F C : ℕ → ℕ → ℚ) (S : ℕ → ℚ) (m : ℕ)
  (nonnegative : ∀ (u : ℕ), ∀ (hu : nat/strict-below u (data/succ (data/succ m))), ∀ (v : ℕ), ∀ (hv : nat/strict-below v (data/succ (data/succ m))), 0 ≤ F u v)
  (capacity : ∀ (u : ℕ), ∀ (hu : nat/strict-below u (data/succ (data/succ m))), ∀ (v : ℕ), ∀ (hv : nat/strict-below v (data/succ (data/succ m))), F u v ≤ C u v)
  (conservation : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun column-index => F (data/succ idx) column-index) (data/succ (data/succ m)) + signed/negate (signed/expr-sum-value (fun row-index => F row-index (data/succ idx)) (data/succ (data/succ m))) = 0)
  (bits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ (data/succ m))), S idx · (1 + signed/negate (S idx)) = 0)
  (source : S 0 = 1)
  (sink : S (data/succ m) = 0)
  → signed/expr-sum-value (fun column-index => F 0 column-index) (data/succ (data/succ m)) + signed/negate (signed/expr-sum-value (fun row-index => F row-index 0) (data/succ (data/succ m))) ≤ signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun i₁ => fun j => S i₁ · (1 + signed/negate (S j)) · C i₁ j) i column-index) (data/succ (data/succ m))) (data/succ (data/succ m))

signed/expr-sum-flat-cut-as-matrix :
  (C S : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun e => S (nat/row-of n e) · (1 + signed/negate (S (nat/col-of n e))) · C e) (nat/multiply n n) = signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun i₁ => fun j => S i₁ · (1 + signed/negate (S j)) · (fun i₂ => fun j₁ => C (algebra/nat-add j₁ (…⟨1⟩ …⟨1⟩ …⟨1⟩))) i₁ j) i column-index) n) n