Reference · Signed rationals

rainbow.math.rational.signed.lp-scaling-feasibility

Signed rationalssrc/rainbow/math/rational/signed/lp_scaling_feasibility.clj0 definitions, 3 theorems

Forward feasibility scaling and universal-bound transport on listed indices. Forward preservation holds for every nonnegative rational D; universal-bound transport uses positive D and the proved original-objective bound theorem. No converse feasibility or candidate-bijection hypothesis is required.

Depends onmath.rational.signed.lp-scaling-boundmath.rational.signed.pointwise-order

signed/scaling-preserves-nonnegative-on.{u} :
  (A : Type u) (d : ℚ≥0) (x : A → ℚ) (cols : List A)
  (nonnegative : ∀ i ∈ cols, 0 ≤ x i)
  → ∀ i ∈ cols, 0 ≤ signed/scale d (x i)

signed/lp-scaling-preserves-primal-feasibility.{u} :
  (A B : Type u) (d : ℚ≥0) (M : A → B → ℚ) (b : A → ℚ) (x : B → ℚ) (rows : List A)
  (cols : List B)
  (feasible : ∀ i ∈ rows, Σ j∈cols, M i j · x j ≤ b i)
  → ∀ i ∈ rows, Σ j∈cols, (fun i₁ => fun j₁ => signed/scale d (M i₁ j₁)) i j · (fun i₁ => signed/scale d (x i₁)) j ≤ signed/scale (d · d) (b i)

signed/lp-scaled-universal-bound-to-original.{u} :
  (A : Type u) (ap adp : ℕ) (M : A → A → ℚ) (b c y : A → ℚ) (rows cols : List A)
  (scaled-universal : ∀ (candidate : A → ℚ), ∀ (feasible : ∀ i ∈ rows, Σ j∈cols, (fun i₁ => fun j₁ => signed/scale (nnrat/make (data/succ ap) adp) (M i₁ j₁)) i j · candidate j ≤ signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) (b i)), ∀ (nonnegative : ∀ i ∈ cols, 0 ≤ candidate i), Σ j∈cols, (fun i => signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) (c i)) j · candidate j ≤ Σ j∈rows, (fun i => signed/scale (nnrat/make (data/succ ap) adp · nnrat/make (data/succ ap) adp) (b i)) j · (fun i => signed/scale (nnrat/make (data/succ ap) adp) (y i)) j)
  (candidate : A → ℚ)
  (feasible : ∀ i ∈ rows, Σ j∈cols, M i j · candidate j ≤ b i)
  (nonnegative : ∀ i ∈ cols, 0 ≤ candidate i)
  → Σ j∈cols, c j · candidate j ≤ Σ j∈rows, b j · y j