Reference · Finite sums

rainbow.math.sums.pareto-mask

Finite sumssrc/rainbow/math/sums/pareto_mask.clj0 definitions, 4 theorems

The Pareto penalty mask is equivalent to absence of strict gain under componentwise dominance.

Depends onmath.sums.indicator-zeromath.sums.zero-violationsmath.sums.nonblockingmath.rational.signed.one-hot-unique

signed/strict-count-below-one-implies-orders :
  (F G : ℕ → ℚ) (n : ℕ)
  (below-one : proposition/negation (1 ≤ signed/expr-sum-value (fun index17618 => data/Bool.rec (fun x₆ => ℚ) 1 0 (signed/decide-at-most (F index17618) (G index17618))) n))
  (idx : ℕ) (bound : nat/strict-below idx n)
  → F idx ≤ G idx

signed/capped-zero-count-is-zero :
  (count : ℚ)
  (zero : count = 0)
  → data/Bool.rec (fun x₄ => ℚ) count 1 (signed/decide-at-most 1 count) = 0

signed/pareto-mask-implies-no-strict-gain :
  (F G : ℕ → ℚ) (n : ℕ)
  (penalty : (1 + signed/negate (data/Bool.rec (fun x₃₄ => ℚ) (signed/expr-sum-value (fun index17640 => data/Bool.rec (fun x₄₀ => ℚ) 1 0 (signed/decide-at-most (F index17640) (G index17640))) n) 1 (signed/decide-at-most 1 (signed/expr-sum-value (fun index17640 => data/Bool.rec (fun x₅₂ => ℚ) 1 0 (signed/decide-at-most (F index17640) (G index17640))) n)))) · signed/expr-sum-value (fun objective17641 => G objective17641 + signed/negate (F objective17641)) n ≤ 0)
  (h₁ : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx)
  (idx : ℕ) (bound : nat/strict-below idx n)
  → G idx = F idx

signed/no-strict-gain-implies-pareto-mask :
  (F G : ℕ → ℚ) (n : ℕ)
  (no-gain : (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ G idx) → (∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), G idx = F idx))
  → (1 + signed/negate (data/Bool.rec (fun x₃₄ => ℚ) (signed/expr-sum-value (fun index17657 => data/Bool.rec (fun x₄₀ => ℚ) 1 0 (signed/decide-at-most (F index17657) (G index17657))) n) 1 (signed/decide-at-most 1 (signed/expr-sum-value (fun index17657 => data/Bool.rec (fun x₅₂ => ℚ) 1 0 (signed/decide-at-most (F index17657) (G index17657))) n)))) · signed/expr-sum-value (fun objective17658 => G objective17658 + signed/negate (F objective17658)) n ≤ 0