Mathlib.Optimization

Optimization helpers staged for Mathlib: exact rational linear programming, weighted-simplex KKT certificates, active-set minimizers, truncation reductions, and boundary-slice selectors.

Affine 26 core · 28 supporting · 1 submodule Affine sign-cell methods for constrained optimization. Quadratic­Saddle 12 core · 18 supporting · 4 submodules This module collects fixed compact-polytope finite quadratic max-min problems, their Borel value and saddle relations, and exact Borel saddle selectors with a fixed fallback outside an attainment domain.
Compact­Saddle­Value 4 core · 5 supporting A jointly continuous objective is maximized over a fixed compact action set and minimized over a scalar decision. ★ continuousAt_value

Continuity of compact saddle values

A jointly continuous objective is maximized over a fixed compact action set and minimized over a scalar decision. When the scalar minimum is attained in one fixed compact set near a parameter, the value and, at a positive value, its reciprocal are continuous without continuity of a selected optimizer.

def envelope reviewed
Causalean.Mathlib.Optimization.CompactSaddleValue

The fixed action set, objective family, parameter, and scalar decision determine the maximum envelope, given by the supremum over the action set as its defining equation.

Definition (Lean source)
parameters
Θ :
Type u_1
shared
A :
Type u_2
shared
S :
Set A
f :
Θ → A → ℝ → ℝ
θ :
Θ
t :
ℝ
def
envelope S f θ t :
ℝ
given by
sSup ((fun a : A => f θ a t) '' S)
Causalean.Mathlib.Optimization.CompactSaddleValue.envelope · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:22
def value reviewed
Causalean.Mathlib.Optimization.CompactSaddleValue

The fixed action set, objective family, and parameter determine the min-max saddle value, given by the infimum over all real scalar decisions of the maximum envelope as its defining equation: the action is maximized first and the scalar decision is minimized second.

Definition (Lean source)
parameters
Θ :
Type u_1
shared
A :
Type u_2
shared
S :
Set A
f :
Θ → A → ℝ → ℝ
θ :
Θ
def
value S f θ :
ℝ
given by
sInf ((fun t : ℝ => envelope S f θ t) '' univ)
Causalean.Mathlib.Optimization.CompactSaddleValue.value · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:28
def compactMin reviewed
Causalean.Mathlib.Optimization.CompactSaddleValue

The fixed action set, objective family, compact scalar set, and parameter determine the compact scalar minimum, given by the infimum of the maximum envelope over that scalar set as its defining equation.

Definition (Lean source)
parameters
Θ :
Type u_1
shared
A :
Type u_2
shared
S :
Set A
f :
Θ → A → ℝ → ℝ
K :
Set ℝ
θ :
Θ
def
compactMin S f K θ :
ℝ
given by
sInf ((fun t : ℝ => envelope S f θ t) '' K)
Causalean.Mathlib.Optimization.CompactSaddleValue.compactMin · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:35
theorem continuousAt_value reviewed
Causalean.Mathlib.Optimization.CompactSaddleValue

A compact nonempty action set, objective family, compact nonempty scalar set, parameter, joint continuity of the objective, and attainment, for every parameter near the given one, of the global scalar minimum of the envelope at a point of the compact set give a min-max saddle value (infimum over scalar decisions of the maximum over actions) that is continuous at the parameter.

Formal statement
hypotheses
Θ :
Type u_1
shared
A :
Type u_2
shared
S :
Set A
hS :
IsCompact S
hSne :
S.Nonempty
f :
Θ → A → ℝ → ℝ
K :
Set ℝ
hK :
IsCompact K
hKne :
K.Nonempty
θ₀ :
Θ
hf :
Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)
hatt :
∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u
conclusion
ContinuousAt (value S f) θ₀
Proof (Lean source)
theorem continuousAt_value (S : Set A) (hS : IsCompact S) (hSne : S.Nonempty) (f : Θ → A → ℝ → ℝ) (K : Set ℝ) (hK : IsCompact K) (hKne : K.Nonempty) (θ₀ : Θ) (hf : Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)) (hatt : ∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u) : ContinuousAt (value S f) θ₀ := by have _hSne : S.Nonempty := hSne have _hKne : K.Nonempty := hKne apply (continuous_compactMin S hS f K hK hf).continuousAt.congr filter_upwards [hatt] with θ ⟨t, ht, hmin⟩ exact (value_eq_compactMin_of_attained S f K θ t ht hmin).symm
Causalean.Mathlib.Optimization.CompactSaddleValue.continuousAt_value · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:79 · uses envelope , value
5 supporting declarations (lemmas, instances)
  • continuous_envelope theorem — A compact action set and jointly continuous objective give a jointly continuous maximum envelope in the parameter and scalar decision.
    hypotheses
    Θ :
    Type u_1
    shared
    A :
    Type u_2
    shared
    S :
    Set A
    hS :
    IsCompact S
    f :
    Θ → A → ℝ → ℝ
    hf :
    Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)
    conclusion
    Continuous (fun x : Θ × ℝ => envelope S f x.1 x.2)
    Proof (Lean source)
    theorem continuous_envelope (S : Set A) (hS : IsCompact S) (f : Θ → A → ℝ → ℝ) (hf : Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)) : Continuous (fun x : Θ × ℝ => envelope S f x.1 x.2) := by exact hS.continuous_sSup hf
    Causalean.Mathlib.Optimization.CompactSaddleValue.continuous_envelope · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:41
  • continuous_compactMin theorem — A compact action set, objective family, compact scalar set, and jointly continuous objective give a continuous compact scalar minimum.
    hypotheses
    Θ :
    Type u_1
    shared
    A :
    Type u_2
    shared
    S :
    Set A
    hS :
    IsCompact S
    f :
    Θ → A → ℝ → ℝ
    K :
    Set ℝ
    hK :
    IsCompact K
    hf :
    Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)
    conclusion
    Continuous (compactMin S f K)
    Proof (Lean source)
    theorem continuous_compactMin (S : Set A) (hS : IsCompact S) (f : Θ → A → ℝ → ℝ) (K : Set ℝ) (hK : IsCompact K) (hf : Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)) : Continuous (compactMin S f K) := by exact hK.continuous_sInf (continuous_envelope S hS f hf)
    Causalean.Mathlib.Optimization.CompactSaddleValue.continuous_compactMin · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:49
  • value_eq_compactMin_of_attained theorem — An action set, objective family, compact scalar set, parameter, and scalar point belonging to that set whose envelope value is no larger than at every scalar point give equality of the unrestricted saddle value and compact scalar minimum.
    hypotheses
    Θ :
    Type u_1
    shared
    A :
    Type u_2
    shared
    S :
    Set A
    f :
    Θ → A → ℝ → ℝ
    K :
    Set ℝ
    θ :
    Θ
    t :
    ℝ
    ht :
    t ∈ K
    hmin :
    ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u
    conclusion
    value S f θ = compactMin S f K θ
    Proof (Lean source)
    theorem value_eq_compactMin_of_attained (S : Set A) (f : Θ → A → ℝ → ℝ) (K : Set ℝ) (θ : Θ) (t : ℝ) (ht : t ∈ K) (hmin : ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u) : value S f θ = compactMin S f K θ := by have hall : IsLeast ((fun u : ℝ => envelope S f θ u) '' univ) (envelope S f θ t) := by constructor · exact ⟨t, Set.mem_univ _, rfl⟩ · rintro y ⟨u, -, rfl⟩ exact hmin u have hcompact : IsLeast ((fun u : ℝ => envelope S f θ u) '' K) (envelope S f θ t) := by constructor · exact ⟨t, ht, rfl⟩ · rintro y ⟨u, -, rfl⟩ exact hmin u exact (hall.csInf_eq).trans hcompact.csInf_eq.symm
    Causalean.Mathlib.Optimization.CompactSaddleValue.value_eq_compactMin_of_attained · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:57
  • continuousAt_inv_value theorem — A compact nonempty action set, objective family, compact nonempty scalar set, parameter, joint continuity of the objective, eventual attainment of scalar envelope minima in the compact set, and a strictly positive saddle value at the parameter give a continuous reciprocal saddle value at that parameter.
    hypotheses
    Θ :
    Type u_1
    shared
    A :
    Type u_2
    shared
    S :
    Set A
    hS :
    IsCompact S
    hSne :
    S.Nonempty
    f :
    Θ → A → ℝ → ℝ
    K :
    Set ℝ
    hK :
    IsCompact K
    hKne :
    K.Nonempty
    θ₀ :
    Θ
    hf :
    Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)
    hatt :
    ∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u
    hpos :
    0 < value S f θ₀
    conclusion
    ContinuousAt (fun θ => (value S f θ)⁻¹) θ₀
    Proof (Lean source)
    theorem continuousAt_inv_value (S : Set A) (hS : IsCompact S) (hSne : S.Nonempty) (f : Θ → A → ℝ → ℝ) (K : Set ℝ) (hK : IsCompact K) (hKne : K.Nonempty) (θ₀ : Θ) (hf : Continuous (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2)) (hatt : ∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u) (hpos : 0 < value S f θ₀) : ContinuousAt (fun θ => (value S f θ)⁻¹) θ₀ := by exact (continuousAt_value S hS hSne f K hK hKne θ₀ hf hatt).inv₀ (ne_of_gt hpos)
    Causalean.Mathlib.Optimization.CompactSaddleValue.continuousAt_inv_value · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:98
  • continuousAt_value_of_continuousOn theorem — A compact nonempty action set, objective family, compact nonempty scalar set, parameter, parameter neighborhood, openness of that neighborhood, and membership of the parameter, joint continuity of the objective on that neighborhood, and eventual attainment of scalar envelope minima in the compact set give a min-max saddle value that is continuous at the parameter.
    hypotheses
    Θ :
    Type u_1
    shared
    A :
    Type u_2
    shared
    S :
    Set A
    hS :
    IsCompact S
    hSne :
    S.Nonempty
    f :
    Θ → A → ℝ → ℝ
    K :
    Set ℝ
    hK :
    IsCompact K
    hKne :
    K.Nonempty
    θ₀ :
    Θ
    U :
    Set Θ
    hUopen :
    IsOpen U
    hθU :
    θ₀ ∈ U
    hf :
    ContinuousOn (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2) {x | x.1.1 ∈ U}
    hatt :
    ∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u
    conclusion
    ContinuousAt (value S f) θ₀
    Proof (Lean source)
    theorem continuousAt_value_of_continuousOn (S : Set A) (hS : IsCompact S) (hSne : S.Nonempty) (f : Θ → A → ℝ → ℝ) (K : Set ℝ) (hK : IsCompact K) (hKne : K.Nonempty) (θ₀ : Θ) (U : Set Θ) (hUopen : IsOpen U) (hθU : θ₀ ∈ U) (hf : ContinuousOn (fun x : (Θ × ℝ) × A => f x.1.1 x.2 x.1.2) {x | x.1.1 ∈ U}) (hatt : ∀ᶠ θ in nhds θ₀, ∃ t ∈ K, ∀ u : ℝ, envelope S f θ t ≤ envelope S f θ u) : ContinuousAt (value S f) θ₀ := by let fU : U → A → ℝ → ℝ := fun θ a t => f θ.1 a t have hfU : Continuous (fun x : (U × ℝ) × A => fU x.1.1 x.2 x.1.2) := by apply continuous_iff_continuousAt.2 intro x have hmap : ContinuousAt (fun y : (U × ℝ) × A => ((y.1.1.1, y.1.2), y.2)) x := by fun_prop exact (hf.continuousAt ((hUopen.preimage (continuous_fst.comp continuous_fst)).mem_nhds x.1.1.2)).comp hmap have hattU : ∀ᶠ θ in nhds (⟨θ₀, hθU⟩ : U), ∃ t ∈ K, ∀ u : ℝ, envelope S fU θ t ≤ envelope S fU θ u := by filter_upwards [(continuous_subtype_val.continuousAt.eventually hatt)] with θ hθ exact hθ have hlocal := continuousAt_value S hS hSne fU K hK hKne (⟨θ₀, hθU⟩ : U) hfU hattU apply (continuousWithinAt_iff_continuousAt (hUopen.mem_nhds hθU)).mp exact (continuousWithinAt_iff_continuousAt_domRestrict (value S f) hθU).mpr hlocal
    Causalean.Mathlib.Optimization.CompactSaddleValue.continuousAt_value_of_continuousOn · Causalean/Mathlib/Optimization/CompactSaddleValue.lean:112
Finite­Knapsack 1 core · 2 supporting Finite fractional-knapsack optimization. ★ finite_knapsack_dual_witness

Finite fractional-knapsack optimization. This module proves attainment on the finite policy box, derives the KKT shadow-price identity, and packages primal attainment with an exact dual representation.

lemma finite_knapsack_dual_witness reviewed
Causalean.Mathlib.Optimization

A finite fractional knapsack with dimension, weights, item values, budget, nonnegative weights, values at most one, and a unit-interval budget certificate admits a feasible primal policy and a unit-interval dual price whose objectives are equal.

Formal statement
hypotheses
d :
ℕ
p tau :
Fin d → ℝ
b :
ℝ
hp :
∀ j, 0 ≤ p j
ht :
∀ j, tau j ≤ 1
hb :
b ∈ Icc (0 : ℝ) 1
conclusion
∃ pi : EuclideanSpace ℝ (Fin d),
conclusion 1
j :
pi j ∈ Icc (0 : ℝ) 1
conclusion 2
(∑ j, p j * pi j) ≤ b
conclusion 3
∃ lambda ∈ Icc (0 : ℝ) 1,
(∑ j, p j * pi j * tau j) = b * lambda + ∑ j, p j * max 0 (tau j - lambda)
Proof (Lean source)
lemma finite_knapsack_dual_witness {d : ℕ} (p tau : Fin d → ℝ) (b : ℝ) (hp : ∀ j, 0 ≤ p j) (ht : ∀ j, tau j ≤ 1) (hb : b ∈ Icc (0 : ℝ) 1) : ∃ pi : EuclideanSpace ℝ (Fin d), (∀ j, pi j ∈ Icc (0 : ℝ) 1) ∧ (∑ j, p j * pi j) ≤ b ∧ ∃ lambda ∈ Icc (0 : ℝ) 1, (∑ j, p j * pi j * tau j) = b * lambda + ∑ j, p j * max 0 (tau j - lambda) := by obtain ⟨pi, hpi, hbudget, hmax⟩ := finite_knapsack_attains p tau b hb.1 obtain ⟨lambda, hlambda, hcomp, hcell⟩ := finite_knapsack_kkt p tau b hp pi hpi hbudget hmax have heq : (∑ j, p j * pi j * tau j) = b * lambda + ∑ j, p j * max 0 (tau j - lambda) := by calc _ = ∑ j, (lambda * (p j * pi j) + p j * max 0 (tau j - lambda)) := by apply Finset.sum_congr rfl intro j _ exact hcell j _ = lambda * (∑ j, p j * pi j) + ∑ j, p j * max 0 (tau j - lambda) := by rw [Finset.sum_add_distrib, Finset.mul_sum] _ = b * lambda + ∑ j, p j * max 0 (tau j - lambda) := by have : lambda * (∑ j, p j * pi j) = lambda * b := by nlinarith [hcomp] rw [this] ring by_cases hlam1 : lambda ≤ 1 · exact ⟨pi, hpi, hbudget, lambda, ⟨hlambda, hlam1⟩, heq⟩ · have hhinge : ∑ j, p j * max 0 (tau j - lambda) = 0 := by apply Finset.sum_eq_zero intro j _ rw [max_eq_left] · ring · linarith [ht j] have hgain_le : (∑ j, p j * pi j * tau j) ≤ ∑ j, p j * pi j := by apply Finset.sum_le_sum intro j _ have hppi : 0 ≤ p j * pi j := mul_nonneg (hp j) (hpi j).1 nlinarith [ht j] have hb0 : b = 0 := by rw [hhinge] at heq have : b * lambda ≤ b := by linarith nlinarith [hb.1] refine ⟨pi, hpi, hbudget, 1, by norm_num, ?_⟩ rw [hb0] have hhinge1 : ∑ j, p j * max 0 (tau j - 1) = 0 := by apply Finset.sum_eq_zero intro j _ rw [max_eq_left] · ring · linarith [ht j] rw [hhinge1] simpa [hb0, hhinge] using heq
Causalean.Mathlib.Optimization.finite_knapsack_dual_witness · Causalean/Mathlib/Optimization/FiniteKnapsack.lean:328
2 supporting declarations (lemmas, instances)
  • finite_knapsack_attains lemma — A finite fractional knapsack with dimension, weights, item values, budget, and a nonnegative-budget certificate has a feasible policy that maximizes the weighted value over every box-constrained policy within budget.
    hypotheses
    d :
    ℕ
    p tau :
    Fin d → ℝ
    b :
    ℝ
    hb :
    0 ≤ b
    conclusion
    ∃ pi : EuclideanSpace ℝ (Fin d),
    conclusion 1
    j :
    pi j ∈ Icc (0 : ℝ) 1
    conclusion 2
    (∑ j, p j * pi j) ≤ b
    conclusion 3
    rho :
    EuclideanSpace ℝ (Fin d)
    (∀ j, rho j ∈ Icc (0 : ℝ) 1)
    (∑ j, p j * rho j) ≤ b
    (∑ j, p j * rho j * tau j) ≤ ∑ j, p j * pi j * tau j
    Proof (Lean source)
    lemma finite_knapsack_attains {d : ℕ} (p tau : Fin d → ℝ) (b : ℝ) (hb : 0 ≤ b) : ∃ pi : EuclideanSpace ℝ (Fin d), (∀ j, pi j ∈ Icc (0 : ℝ) 1) ∧ (∑ j, p j * pi j) ≤ b ∧ ∀ rho : EuclideanSpace ℝ (Fin d), (∀ j, rho j ∈ Icc (0 : ℝ) 1) → (∑ j, p j * rho j) ≤ b → (∑ j, p j * rho j * tau j) ≤ ∑ j, p j * pi j * tau j := by classical let box : Set (EuclideanSpace ℝ (Fin d)) := toLp 2 '' pi univ (fun _ : Fin d => Icc (0 : ℝ) 1) let cost : EuclideanSpace ℝ (Fin d) → ℝ := fun x => ∑ j, p j * x j let value : EuclideanSpace ℝ (Fin d) → ℝ := fun x => ∑ j, p j * x j * tau j have hbox : IsCompact box := by exact (isCompact_univ_pi fun _ : Fin d => isCompact_Icc).image (PiLp.continuous_toLp 2 (fun _ : Fin d => ℝ)) have hcost : Continuous cost := by dsimp [cost] fun_prop have hvalue : Continuous value := by dsimp [value] fun_prop let K := box ∩ {x | cost x ≤ b} have hK : IsCompact K := hbox.inter_right (isClosed_le hcost continuous_const) have h0box : (0 : EuclideanSpace ℝ (Fin d)) ∈ box := by refine ⟨0, ?_, ?_⟩ · intro j _ norm_num · rfl have h0K : (0 : EuclideanSpace ℝ (Fin d)) ∈ K := by exact ⟨h0box, by simpa [cost] using hb⟩ obtain ⟨pi, hpiK, hpiMax⟩ := hK.exists_isMaxOn ⟨0, h0K⟩ hvalue.continuousOn refine ⟨pi, ?_, hpiK.2, ?_⟩ · rintro j obtain ⟨x, hx, rfl⟩ := hpiK.1 exact hx j (Set.mem_univ j) · intro rho hrho hcostrho apply hpiMax refine ⟨?_, hcostrho⟩ refine ⟨fun j => rho j, ?_, ?_⟩ intro j _ exact hrho j ext j rfl
    Causalean.Mathlib.Optimization.finite_knapsack_attains · Causalean/Mathlib/Optimization/FiniteKnapsack.lean:18
  • finite_knapsack_kkt lemma — For a finite fractional knapsack with dimension, weights, item values, budget, nonnegative weights, a box-constrained feasible policy, and its maximizing certificate, there is a nonnegative shadow price satisfying complementary slackness and the coordinatewise hinge-value identity.
    hypotheses
    d :
    ℕ
    p tau :
    Fin d → ℝ
    b :
    ℝ
    hp :
    ∀ j, 0 ≤ p j
    pi :
    EuclideanSpace ℝ (Fin d)
    hpi :
    ∀ j, pi j ∈ Icc (0 : ℝ) 1
    hbudget :
    (∑ j, p j * pi j) ≤ b
    hmax :
    ∀ rho : EuclideanSpace ℝ (Fin d)
    if
    (∀ j, rho j ∈ Icc (0 : ℝ) 1)
    and
    (∑ j, p j * rho j) ≤ b
    then
    (∑ j, p j * rho j * tau j) ≤ ∑ j, p j * pi j * tau j
    conclusion
    ∃ lambda : ℝ,
    0 ≤ lambda
    lambda * (b - ∑ j, p j * pi j) = 0
    conclusion 1
    j :
    p j * pi j * tau j = lambda * (p j * pi j) + p j * max 0 (tau j - lambda)
    Proof (Lean source)
    lemma finite_knapsack_kkt {d : ℕ} (p tau : Fin d → ℝ) (b : ℝ) (hp : ∀ j, 0 ≤ p j) (pi : EuclideanSpace ℝ (Fin d)) (hpi : ∀ j, pi j ∈ Icc (0 : ℝ) 1) (hbudget : (∑ j, p j * pi j) ≤ b) (hmax : ∀ rho : EuclideanSpace ℝ (Fin d), (∀ j, rho j ∈ Icc (0 : ℝ) 1) → (∑ j, p j * rho j) ≤ b → (∑ j, p j * rho j * tau j) ≤ ∑ j, p j * pi j * tau j) : ∃ lambda : ℝ, 0 ≤ lambda ∧ lambda * (b - ∑ j, p j * pi j) = 0 ∧ ∀ j, p j * pi j * tau j = lambda * (p j * pi j) + p j * max 0 (tau j - lambda) := by classical let κ := Option (Fin d ⊕ Fin d) let N := Fintype.card κ let e : Fin N ≃ κ := (Fintype.equivFin κ).symm let sigma : Finset ℕ := Finset.range N let pvec : EuclideanSpace ℝ (Fin d) := toLp 2 p let tvec : EuclideanSpace ℝ (Fin d) := toLp 2 (fun j => p j * tau j) let row : κ → EuclideanSpace ℝ (Fin d) | none => -pvec | some (inl j) => single j 1 | some (inr j) => -single j 1 let offset : κ → ℝ | none => b | some (inl _) => 0 | some (inr _) => 1 let constraint : ℕ → EuclideanSpace ℝ (Fin d) → ℝ := fun i x => if hi : i < N then inner ℝ x (row (e ⟨i, hi⟩)) + offset (e ⟨i, hi⟩) else 0 let P : Constrained_OptimizationProblem (EuclideanSpace ℝ (Fin d)) ∅ sigma := { domain := univ equality_constraints := fun _ _ => 0 inequality_constraints := constraint eq_ine_not_intersect := by simp objective := fun x => inner ℝ x (-tvec) } have hinner_p (x : EuclideanSpace ℝ (Fin d)) : inner ℝ x pvec = ∑ j, p j * x j := by simp [pvec, EuclideanSpace.inner_eq_star_dotProduct, dotProduct, mul_comm] have hinner_t (x : EuclideanSpace ℝ (Fin d)) : inner ℝ x tvec = ∑ j, p j * x j * tau j := by simp [tvec, EuclideanSpace.inner_eq_star_dotProduct, dotProduct] apply Finset.sum_congr rfl intro j _ ring have hconstraint_none (x : EuclideanSpace ℝ (Fin d)) : constraint (e.symm none).val x = b - ∑ j, p j * x j := by rw [show constraint (e.symm none).val x = inner ℝ x (row none) + offset none by simp [constraint, (e.symm none).isLt]] simp [row, offset, hinner_p] ring have hconstraint_lower (x : EuclideanSpace ℝ (Fin d)) (j : Fin d) : constraint (e.symm (some (inl j))).val x = x j := by rw [show constraint (e.symm (some (inl j))).val x = inner ℝ x (row (some (inl j))) + offset (some (inl j)) by simp [constraint, (e.symm (some (inl j))).isLt]] simp [row, offset, EuclideanSpace.inner_single_right] have hconstraint_upper (x : EuclideanSpace ℝ (Fin d)) (j : Fin d) : constraint (e.symm (some (inr j))).val x = 1 - x j := by rw [show constraint (e.symm (some (inr j))).val x = inner ℝ x (row (some (inr j))) + offset (some (inr j)) by simp [constraint, (e.symm (some (inr j))).isLt]] simp [row, offset, EuclideanSpace.inner_single_right] ring have hfeas : P.FeasPoint pi := by refine ⟨Set.mem_univ _, by simp, ?_⟩ intro i hi have hiN : i < N := Finset.mem_range.mp hi generalize hc : e ⟨i, hiN⟩ = c rcases c with _ | (j | j) · have hcode : i = (e.symm none).val := by have := congrArg (fun z => (e.symm z).val) hc simpa using this rw [hcode] change constraint (e.symm none).val pi ≥ 0 rw [hconstraint_none] linarith · have hcode : i = (e.symm (some (inl j))).val := by have := congrArg (fun z => (e.symm z).val) hc simpa using this rw [hcode] change constraint (e.symm (some (inl j))).val pi ≥ 0 rw [hconstraint_lower] exact (hpi j).1 · have hcode : i = (e.symm (some (inr j))).val := by have := congrArg (fun z => (e.symm z).val) hc simpa using this rw [hcode] change constraint (e.symm (some (inr j))).val pi ≥ 0 rw [hconstraint_upper] linarith [(hpi j).2] have hlocal : P.Local_Minimum pi := by refine ⟨hfeas, ?_⟩ apply IsMinOn.localize intro rho hrho have hrho' : P.FeasPoint rho := hrho have hlower (j : Fin d) : 0 ≤ rho j := by have hm := hrho'.2.2 (e.symm (some (inl j))).val (Finset.mem_range.mpr (e.symm (some (inl j))).isLt) change constraint (e.symm (some (inl j))).val rho ≥ 0 at hm rwa [hconstraint_lower] at hm have hupper (j : Fin d) : rho j ≤ 1 := by have hm := hrho'.2.2 (e.symm (some (inr j))).val (Finset.mem_range.mpr (e.symm (some (inr j))).isLt) change constraint (e.symm (some (inr j))).val rho ≥ 0 at hm rw [hconstraint_upper] at hm linarith have hcostrho : (∑ j, p j * rho j) ≤ b := by have hm := hrho'.2.2 (e.symm none).val (Finset.mem_range.mpr (e.symm none).isLt) change constraint (e.symm none).val rho ≥ 0 at hm rw [hconstraint_none] at hm linarith simpa [P, hinner_t] using neg_le_neg (hmax rho (fun j => ⟨hlower j, hupper j⟩) hcostrho) have hdiff : Differentiable ℝ P.objective := by intro x dsimp [P] simpa only [real_inner_comm] using (gradient_of_inner_const x (-tvec)).differentiableAt have hcont : ∀ i ∈ sigma, ContDiffAt ℝ (1 : ℕ) (P.inequality_constraints i) pi := by intro i hi dsimp [P, constraint] split_ifs with hiN · have hc : ContDiff ℝ (1 : ℕ) (fun x : EuclideanSpace ℝ (Fin d) => inner ℝ (row (e ⟨i, hiN⟩)) x + offset (e ⟨i, hiN⟩)) := by exact (innerSL ℝ (row (e ⟨i, hiN⟩))).contDiff.add contDiff_const simpa only [real_inner_comm] using hc.contDiffAt · exact contDiffAt_const have hlin : P.LinearCQ pi := by constructor · simp · intro i hi refine ⟨if hiN : i < N then row (e ⟨i, hiN⟩) else 0, if hiN : i < N then offset (e ⟨i, hiN⟩) else 0, ?_⟩ funext x simp only [P, constraint] split_ifs <;> simp obtain ⟨_, eta, mu, hstationary, hmu, hcomp⟩ := first_order_neccessary_LinearCQ P pi hlocal hdiff (by simp) hcont hlin rfl let idx (c : κ) : sigma := ⟨(e.symm c).val, Finset.mem_range.mpr (e.symm c).isLt⟩ let lambda := mu (idx none) let lower (j : Fin d) := mu (idx (some (inl j))) let upper (j : Fin d) := mu (idx (some (inr j))) have hlambda : 0 ≤ lambda := hmu (idx none) have hlower_mu (j : Fin d) : 0 ≤ lower j := hmu (idx (some (inl j))) have hupper_mu (j : Fin d) : 0 ≤ upper j := hmu (idx (some (inr j))) have hcomp_budget : lambda * (b - ∑ j, p j * pi j) = 0 := by have hc := hcomp (idx none) change mu (idx none) * constraint (e.symm none).val pi = 0 at hc rwa [hconstraint_none] at hc have hcomp_lower (j : Fin d) : lower j * pi j = 0 := by have hc := hcomp (idx (some (inl j))) change mu (idx (some (inl j))) * constraint (e.symm (some (inl j))).val pi = 0 at hc rwa [hconstraint_lower] at hc have hcomp_upper (j : Fin d) : upper j * (1 - pi j) = 0 := by have hc := hcomp (idx (some (inr j))) change mu (idx (some (inr j))) * constraint (e.symm (some (inr j))).val pi = 0 at hc rwa [hconstraint_upper] at hc -- Stationarity identifies the reduced costs coordinate by coordinate. have hstationary_coord (j : Fin d) : p j * (lambda - tau j) - lower j + upper j = 0 := by let es : sigma ≃ κ := { toFun := fun q => e ⟨q.val, Finset.mem_range.mp q.property⟩ invFun := fun c => idx c left_inv := by intro q apply Subtype.ext simp [idx] right_inv := by intro c simp [idx] } let v : EuclideanSpace ℝ (Fin d) := -tvec - ∑ q : sigma, mu q • row (es q) let c0 : ℝ := -∑ q : sigma, mu q * offset (es q) have hconstraint_es (q : sigma) (x : EuclideanSpace ℝ (Fin d)) : constraint q.val x = inner ℝ x (row (es q)) + offset (es q) := by unfold constraint rw [dif_pos (Finset.mem_range.mp q.property)] simp [es] have hLag : (fun x => P.Lagrange_function x eta mu) = fun x => inner ℝ v x + c0 := by funext x simp only [Constrained_OptimizationProblem.Lagrange_function, P, Finset.sum_empty, zero_sub] simp_rw [hconstraint_es] simp only [mul_add, Finset.sum_add_distrib, Finset.sum_const_zero, Finset.card_empty, Nat.cast_zero, zero_mul, sub_zero] simp [v, c0, inner_sub_left, inner_neg_left, inner_sum, inner_smul_left, inner_smul_right, real_inner_comm] ring rw [hLag, gradient_add_const] at hstationary rw [(gradient_of_inner_const pi v).gradient] at hstationary have hvj := congrArg (fun z : EuclideanSpace ℝ (Fin d) => inner ℝ (single j 1) z) hstationary have hes_symm (c : κ) : es.symm c = idx c := rfl have hsum : (∑ q : sigma, inner ℝ (single j 1) (mu q • row (es q))) = -lambda * p j + lower j - upper j := by rw [Fintype.sum_equiv es (fun q : sigma => inner ℝ (single j 1) (mu q • row (es q))) (fun c : κ => inner ℝ (single j 1) (mu (es.symm c) • row c)) (fun q => by rw [es.symm_apply_apply])] rw [Fintype.sum_option, Fintype.sum_sum_type] simp_rw [inner_smul_right, EuclideanSpace.inner_single_left] simp [hes_symm, idx, lambda, lower, upper, row, pvec, PiLp.single_apply] ring simp only [v, inner_sub_right, inner_neg_right, inner_sum] at hvj rw [hsum] at hvj rw [EuclideanSpace.inner_single_left] at hvj simp [tvec] at hvj linarith refine ⟨lambda, hlambda, hcomp_budget, ?_⟩ intro j by_cases hp0 : p j = 0 · simp [hp0] rcases hpi j with ⟨hpi0, hpi1⟩ by_cases hj0 : pi j = 0 · have hu0 : upper j = 0 := by have hc := hcomp_upper j rw [hj0] at hc simpa using hc have hred : 0 ≤ lambda - tau j := by have hs := hstationary_coord j have hp_nonneg : 0 ≤ p j := hp j have hp_pos := lt_of_le_of_ne hp_nonneg (Ne.symm hp0) rw [hu0] at hs nlinarith [hlower_mu j] rw [hj0, max_eq_left (by linarith : tau j - lambda ≤ 0)] ring · have hl0 : lower j = 0 := by exact (mul_eq_zero.mp (hcomp_lower j)).resolve_right hj0 by_cases hj1 : pi j = 1 · have hs := hstationary_coord j rw [hl0] at hs have heq : p j * max 0 (tau j - lambda) = p j * (tau j - lambda) := by have hp_pos := lt_of_le_of_ne (hp j) (Ne.symm hp0) rw [max_eq_right] nlinarith [hupper_mu j] rw [hj1, heq] ring -- … truncated; follow the source link for the rest …
    Causalean.Mathlib.Optimization.finite_knapsack_kkt · Causalean/Mathlib/Optimization/FiniteKnapsack.lean:67
Finite­Support 3 core · 3 supporting This module proves the finite basic-feasible-solution sparsity principle for a nonnegative real linear program with equality moments. ★ exists_sparse_maximizer

Sparse finite linear-program maximizers

This module proves the finite basic-feasible-solution sparsity principle for a nonnegative real linear program with equality moments. It preserves any one additional scalar moment without treating the objective as an extra independent constraint, and it works with repeated indexed coefficient columns.

def weightSupport reviewed
Causalean.Mathlib.Optimization

The indexed support of a finite real weight vector consists of exactly the coordinates carrying nonzero weights.

Definition (Lean source)
parameters
ι :
Type u_1
shared
x :
ι → ℝ
def
weightSupport x :
Finset ι
given by
Finset.univ.filter (fun i => x i ≠ 0)
Causalean.Mathlib.Optimization.weightSupport · Causalean/Mathlib/Optimization/FiniteSupport.lean:20
def moment reviewed
Causalean.Mathlib.Optimization

The scalar moment of a coefficient vector against a finite real weight vector is their finite coordinate pairing.

Definition (Lean source)
parameters
ι :
Type u_1
shared
a x :
ι → ℝ
def
moment a x :
ℝ
given by
∑ i, a i * x i
Causalean.Mathlib.Optimization.moment · Causalean/Mathlib/Optimization/FiniteSupport.lean:25
theorem exists_sparse_maximizer reviewed
Causalean.Mathlib.Optimization

Given base moment coefficients, prescribed base moments, an additional scalar coefficient, an objective coefficient, and an initial nonnegative globally maximizing feasible vector, there is a nonnegative global maximizer with the same base, additional, and objective moments and at most one more nonzero coordinate than the number of base moments. Repeated indexed coefficient columns are allowed.

Formal statement
hypotheses
ι κ :
Type*
Fintype ι
Fintype κ
A :
κ → ι → ℝ
b :
κ → ℝ
g c x :
ι → ℝ
hxnonneg :
∀ i, 0 ≤ x i
hxmoment :
∀ k, moment (A k) x = b k
hmax :
∀ z : ι → ℝ
if
(∀ i, 0 ≤ z i)
and
(∀ k, moment (A k) z = b k)
then
moment c z ≤ moment c x
conclusion
∃ y : ι → ℝ,
conclusion 1
i :
0 ≤ y i
conclusion 2
k :
moment (A k) y = b k
conclusion 3
moment g y = moment g x
conclusion 4
moment c y = moment c x
conclusion 5
(weightSupport y).card ≤ card κ + 1
conclusion 6
z :
ι → ℝ
(∀ i, 0 ≤ z i)
(∀ k, moment (A k) z = b k)
moment c z ≤ moment c y
Proof (Lean source)
theorem exists_sparse_maximizer {ι κ : Type*} [Fintype ι] [Fintype κ] (A : κ → ι → ℝ) (b : κ → ℝ) (g c x : ι → ℝ) (hxnonneg : ∀ i, 0 ≤ x i) (hxmoment : ∀ k, moment (A k) x = b k) (hmax : ∀ z : ι → ℝ, (∀ i, 0 ≤ z i) → (∀ k, moment (A k) z = b k) → moment c z ≤ moment c x) : ∃ y : ι → ℝ, (∀ i, 0 ≤ y i) ∧ (∀ k, moment (A k) y = b k) ∧ moment g y = moment g x ∧ moment c y = moment c x ∧ (weightSupport y).card ≤ card κ + 1 ∧ (∀ z : ι → ℝ, (∀ i, 0 ≤ z i) → (∀ k, moment (A k) z = b k) → moment c z ≤ moment c y) := by classical let P : ℕ → Prop := fun n => ∃ y : ι → ℝ, (∀ i, 0 ≤ y i) ∧ (∀ k, moment (A k) y = b k) ∧ moment g y = moment g x ∧ moment c y = moment c x ∧ (weightSupport y).card = n have hex : ∃ n, P n := by refine ⟨(weightSupport x).card, x, hxnonneg, hxmoment, rfl, rfl, rfl⟩ obtain ⟨y, hynonneg, hymoment, hyg, hyc, hycard⟩ := Nat.find_spec hex have hymax : ∀ z : ι → ℝ, (∀ i, 0 ≤ z i) → (∀ k, moment (A k) z = b k) → moment c z ≤ moment c y := by intro z hznonneg hzmoment rw [hyc] exact hmax z hznonneg hzmoment have hmin (z : ι → ℝ) (hznonneg : ∀ i, 0 ≤ z i) (hzmoment : ∀ k, moment (A k) z = b k) (hzg : moment g z = moment g x) (hzc : moment c z = moment c x) : (weightSupport y).card ≤ (weightSupport z).card := by rw [hycard] exact Nat.find_min' hex ⟨z, hznonneg, hzmoment, hzg, hzc, rfl⟩ have hcard : (weightSupport y).card ≤ card κ + 1 := by by_contra h have hlarge : card κ + 1 < (weightSupport y).card := by omega obtain ⟨d, hdne, hdsupp, hdA, hdg⟩ := exists_kernel_direction A g y hlarge have hdc : moment c d = 0 := objective_orthogonal_of_maximal A b c y d hynonneg hymoment hymax hdsupp hdA obtain ⟨t, hnonneg, hlt⟩ := exists_boundary_perturbation y d hynonneg hdne hdsupp let z : ι → ℝ := fun i => y i + t * d i have hmoment (a : ι → ℝ) : moment a z = moment a y + t * moment a d := by simp only [moment, z, mul_add, Finset.sum_add_distrib, Finset.mul_sum] congr 1 apply Finset.sum_congr rfl intro i hi ring have hzA : ∀ k, moment (A k) z = b k := by intro k rw [hmoment, hdA k, mul_zero, add_zero] exact hymoment k have hzg : moment g z = moment g x := by rw [hmoment, hdg, mul_zero, add_zero] exact hyg have hzc : moment c z = moment c x := by rw [hmoment, hdc, mul_zero, add_zero] exact hyc have hle := hmin z hnonneg hzA hzg hzc exact (not_lt_of_ge hle) hlt exact ⟨y, hynonneg, hymoment, hyg, hyc, hcard, hymax⟩
Causalean.Mathlib.Optimization.exists_sparse_maximizer · Causalean/Mathlib/Optimization/FiniteSupport.lean:235 · uses moment , weightSupport
3 supporting declarations (lemmas, instances)
  • exists_boundary_perturbation theorem — A nonnegative finite weight vector and a nonzero direction that vanishes outside its nonzero coordinates have a nonnegative boundary perturbation with strictly smaller indexed support. No assumption on the signs of the direction is needed.
    hypotheses
    ι :
    Type*
    Fintype ι
    x d :
    ι → ℝ
    hxnonneg :
    ∀ i, 0 ≤ x i
    hdnonzero :
    d ≠ 0
    hsupp :
    ∀ i
    if
    x i = 0
    then
    d i = 0
    conclusion
    ∃ t : ℝ,
    conclusion 1
    i :
    0 ≤ x i + t * d i
    conclusion 2
    (weightSupport (fun i => x i + t * d i)).card < (weightSupport x).card
    Proof (Lean source)
    theorem exists_boundary_perturbation {ι : Type*} [Fintype ι] (x d : ι → ℝ) (hxnonneg : ∀ i, 0 ≤ x i) (hdnonzero : d ≠ 0) (hsupp : ∀ i, x i = 0 → d i = 0) : ∃ t : ℝ, (∀ i, 0 ≤ x i + t * d i) ∧ (weightSupport (fun i => x i + t * d i)).card < (weightSupport x).card := by classical have move (v : ι → ℝ) (hv : ∃ i, 0 < v i) (hvsupp : ∀ i, x i = 0 → v i = 0) : ∃ r : ℝ, (∀ i, 0 ≤ x i - r * v i) ∧ (weightSupport (fun i => x i - r * v i)).card < (weightSupport x).card := by let s : Finset ι := Finset.univ.filter (fun i => 0 < v i) have hs : s.Nonempty := by obtain ⟨i, hi⟩ := hv exact ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hi⟩⟩ obtain ⟨j, hj, hmin⟩ := s.exists_min_image (fun i => x i / v i) hs have hvj : 0 < v j := (Finset.mem_filter.mp hj).2 let r := x j / v j have hr : 0 ≤ r := div_nonneg (hxnonneg j) (le_of_lt hvj) have hnonneg : ∀ i, 0 ≤ x i - r * v i := by intro i by_cases hvi : 0 < v i · have hle : r ≤ x i / v i := hmin i (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hvi⟩) have hmul : r * v i ≤ x i := (le_div_iff₀ hvi).mp hle linarith · have hvi' : v i ≤ 0 := le_of_not_gt hvi have hprod : r * v i ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hr hvi' linarith [hxnonneg i] have hz : x j - r * v j = 0 := by dsimp [r] field_simp ring have hjx : j ∈ weightSupport x := by simp only [weightSupport, mem_filter, Finset.mem_univ, true_and] intro hxj exact (not_lt_of_ge (hvsupp j hxj).le) hvj have hjnew : j ∉ weightSupport (fun i => x i - r * v i) := by simp [weightSupport, hz] have hsub : weightSupport (fun i => x i - r * v i) ⊆ weightSupport x := by intro i hi simp only [weightSupport, mem_filter, Finset.mem_univ, true_and] at hi ⊢ intro hxi simp [hxi, hvsupp i hxi] at hi refine ⟨r, hnonneg, Finset.card_lt_card ?_⟩ exact (Finset.ssubset_iff_of_subset hsub).2 ⟨j, hjx, hjnew⟩ have ⟨i₀, hi₀⟩ : ∃ i, d i ≠ 0 := by by_contra h simp only [not_exists, not_not] at h apply hdnonzero funext i exact h i by_cases hpos : 0 < d i₀ · obtain ⟨r, hr, hc⟩ := move d ⟨i₀, hpos⟩ hsupp refine ⟨-r, ?_, ?_⟩ · intro i simpa [sub_eq_add_neg, mul_comm, mul_left_comm, mul_assoc] using hr i · convert hc using 1 congr 2 ext i ring · have hneg : d i₀ < 0 := lt_of_le_of_ne (le_of_not_gt hpos) hi₀ obtain ⟨r, hr, hc⟩ := move (fun i => -d i) ⟨i₀, by simpa using hneg⟩ (by intro i hi; simp [hsupp i hi]) refine ⟨r, ?_, ?_⟩ · intro i convert hr i using 1 ring · convert hc using 1 congr 2 ext i ring
    Causalean.Mathlib.Optimization.exists_boundary_perturbation · Causalean/Mathlib/Optimization/FiniteSupport.lean:29
  • exists_kernel_direction theorem — Given base moment coefficients, an additional scalar coefficient, and a finite real weight vector whose indexed support exceeds the number of base moments plus one, there is a nonzero direction supported on that support whose base and additional moments all vanish. The coefficient columns may repeat or be linearly dependent.
    hypotheses
    ι κ :
    Type*
    Fintype ι
    Fintype κ
    A :
    κ → ι → ℝ
    g :
    ι → ℝ
    x :
    ι → ℝ
    hlarge :
    card κ + 1 < (weightSupport x).card
    conclusion
    ∃ d : ι → ℝ,
    d ≠ 0
    conclusion 1
    i :
    x i = 0
    d i = 0
    conclusion 2
    k :
    moment (A k) d = 0
    conclusion 3
    moment g d = 0
    Proof (Lean source)
    theorem exists_kernel_direction {ι κ : Type*} [Fintype ι] [Fintype κ] (A : κ → ι → ℝ) (g : ι → ℝ) (x : ι → ℝ) (hlarge : card κ + 1 < (weightSupport x).card) : ∃ d : ι → ℝ, d ≠ 0 ∧ (∀ i, x i = 0 → d i = 0) ∧ (∀ k, moment (A k) d = 0) ∧ moment g d = 0 := by classical let S := weightSupport x let L : (S → ℝ) →ₗ[ℝ] ((κ ⊕ Unit) → ℝ) := { toFun := fun v t => ∑ i : S, (elim A (fun _ => g) t) i.1 * v i map_add' := by intro u v ext t simp [mul_add, Finset.sum_add_distrib] map_smul' := by intro c v ext t simp [smul_eq_mul, Finset.mul_sum, mul_left_comm] } have hdim : finrank ℝ ((κ ⊕ Unit) → ℝ) < finrank ℝ (S → ℝ) := by simpa [S, Fintype.card_sum] using hlarge obtain ⟨v, hv, hvne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot (LinearMap.ker_ne_bot_of_finrank_lt hdim : ker L ≠ ⊥) let d : ι → ℝ := fun i => if h : i ∈ S then v ⟨i, h⟩ else 0 have hsum (a : ι → ℝ) : moment a d = ∑ i : S, a i.1 * v i := by simp only [moment] calc (∑ i : ι, a i * d i) = ∑ i ∈ S, a i * d i := by symm apply Finset.sum_subset (Finset.subset_univ S) intro i hi hiS simp [d, hiS] _ = ∑ i : S, a i.1 * v i := by rw [← Finset.sum_attach] simp [d, Finset.univ_eq_attach] refine ⟨d, ?_, ?_, ?_, ?_⟩ · intro hd apply hvne funext i have hi : d i.1 = v i := by simp [d, i.2] rw [hd] at hi exact hi.symm · intro i hxi have hi : i ∉ S := by simp [S, weightSupport, hxi] simp [d, hi] · intro k have hk := congrFun (show L v = 0 from hv) (inl k) simpa [L, hsum] using hk · have hg := congrFun (show L v = 0 from hv) (inr ()) simpa [L, hsum] using hg
    Causalean.Mathlib.Optimization.exists_kernel_direction · Causalean/Mathlib/Optimization/FiniteSupport.lean:104
  • objective_orthogonal_of_maximal theorem — Given base moment coefficients, prescribed base moments, an objective coefficient, a nonnegative base-feasible vector that globally maximizes the objective among such vectors, and a supported base-moment-kernel direction, the objective moment of that direction is zero.
    hypotheses
    ι κ :
    Type*
    Fintype ι
    A :
    κ → ι → ℝ
    b :
    κ → ℝ
    c x d :
    ι → ℝ
    hxnonneg :
    ∀ i, 0 ≤ x i
    hxmoment :
    ∀ k, moment (A k) x = b k
    hmax :
    ∀ z : ι → ℝ
    if
    (∀ i, 0 ≤ z i)
    and
    (∀ k, moment (A k) z = b k)
    then
    moment c z ≤ moment c x
    hsupp :
    ∀ i
    if
    x i = 0
    then
    d i = 0
    hkernel :
    ∀ k, moment (A k) d = 0
    conclusion
    moment c d = 0
    Proof (Lean source)
    theorem objective_orthogonal_of_maximal {ι κ : Type*} [Fintype ι] (A : κ → ι → ℝ) (b : κ → ℝ) (c x d : ι → ℝ) (hxnonneg : ∀ i, 0 ≤ x i) (hxmoment : ∀ k, moment (A k) x = b k) (hmax : ∀ z : ι → ℝ, (∀ i, 0 ≤ z i) → (∀ k, moment (A k) z = b k) → moment c z ≤ moment c x) (hsupp : ∀ i, x i = 0 → d i = 0) (hkernel : ∀ k, moment (A k) d = 0) : moment c d = 0 := by classical have hcoordinate (i : ι) : ∃ r : ℝ, 0 < r ∧ r * |d i| ≤ x i := by by_cases hx : x i = 0 · refine ⟨1, by norm_num, ?_⟩ simp [hsupp i hx, hx] · have hxpos : 0 < x i := lt_of_le_of_ne (hxnonneg i) (Ne.symm hx) refine ⟨x i / (|d i| + 1), by positivity, ?_⟩ have hden : 0 < |d i| + 1 := by positivity have heq : (x i / (|d i| + 1)) * (|d i| + 1) = x i := div_mul_cancel₀ (x i) (ne_of_gt hden) nlinarith [abs_nonneg (d i)] have hfinite (s : Finset ι) : ∃ r : ℝ, 0 < r ∧ ∀ i ∈ s, r * |d i| ≤ x i := by induction s using Finset.induction_on with | empty => exact ⟨1, by norm_num, by simp⟩ | @insert i s hi ih => obtain ⟨r, hr, hbound⟩ := ih obtain ⟨t, ht, htbound⟩ := hcoordinate i refine ⟨min r t, lt_min hr ht, ?_⟩ intro j hj rcases Finset.mem_insert.mp hj with rfl | hj · exact (mul_le_mul_of_nonneg_right (min_le_right r t) (abs_nonneg _)).trans htbound · exact (mul_le_mul_of_nonneg_right (min_le_left r t) (abs_nonneg _)).trans (hbound j hj) obtain ⟨ε, hε, hεbound⟩ := hfinite univ have hplus_nonneg (i : ι) : 0 ≤ x i + ε * d i := by have hb := hεbound i (Finset.mem_univ i) have hd : 0 ≤ ε * (|d i| + d i) := mul_nonneg hε.le (by linarith [neg_le_abs (d i)]) nlinarith have hminus_nonneg (i : ι) : 0 ≤ x i - ε * d i := by have hb := hεbound i (Finset.mem_univ i) have hd : 0 ≤ ε * (|d i| - d i) := mul_nonneg hε.le (sub_nonneg.mpr (le_abs_self (d i))) nlinarith have hplus (a : ι → ℝ) : moment a (fun i => x i + ε * d i) = moment a x + ε * moment a d := by simp only [moment, mul_add, Finset.sum_add_distrib, Finset.mul_sum] congr 1 apply Finset.sum_congr rfl intro i hi ring have hminus (a : ι → ℝ) : moment a (fun i => x i - ε * d i) = moment a x - ε * moment a d := by simp only [moment, mul_sub, Finset.sum_sub_distrib, Finset.mul_sum] congr 1 apply Finset.sum_congr rfl intro i hi ring have hp := hmax (fun i => x i + ε * d i) hplus_nonneg (by intro k rw [hplus, hkernel k, mul_zero, add_zero] exact hxmoment k) have hm := hmax (fun i => x i - ε * d i) hminus_nonneg (by intro k rw [hminus, hkernel k, mul_zero, sub_zero] exact hxmoment k) rw [hplus] at hp rw [hminus] at hm nlinarith
    Causalean.Mathlib.Optimization.objective_orthogonal_of_maximal · Causalean/Mathlib/Optimization/FiniteSupport.lean:160
Rational­LP 14 core · 3 supporting This module proves attainment and strong duality for a finite linear program whose variables and coefficients are rational. ★ exists_rational_optimal_primal_dual

Exact certificates for rational linear programs

This module proves attainment and strong duality for a finite linear program whose variables and coefficients are rational. The proof uses certified Fourier--Motzkin elimination: primal variables are eliminated while the objective coordinate is retained, and every generated inequality records its nonnegative rational combination of the original rows. The lower endpoint of the resulting one-dimensional rational polyhedron is rational; elimination back-substitution gives a rational primal optimizer, while the recorded combination gives rational nonnegative dual multipliers of the same value.

The standard form minimizes c ⬝ᵥ x subject to A i ⬝ᵥ x ≤ b i, where ⬝ᵥ is Mathlib's dotProduct. Variables are unrestricted in sign. Equalities are represented by pairs of opposite inequalities, while a nonnegativity restriction 0 ≤ x_j is the single inequality -x_j ≤ 0. Thus this form faithfully covers arbitrary finite rational LPs.

structure AugmentedIneq reviewed
Causalean.Mathlib.Optimization.RationalLP

A linear inequality in ordinary variables x and a retained objective coordinate t, written a · x + s * t ≤ b.

Definition (Lean source)
parameters
n :
ℕ
fields
Coefficients of the ordinary variables.
coeff :
Fin n → ℚ
Coefficient of the retained objective coordinate.
objCoeff :
ℚ
Right-hand side.
rhs :
ℚ
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq · Causalean/Mathlib/Optimization/RationalLP.lean:49
def Holds reviewed
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq

Given a number of ordinary coordinates, an augmented rational inequality, a rational ordinary-variable vector, and a retained rational objective coordinate, the inequality-satisfaction condition holds exactly when the dot product of the ordinary coefficients and vector plus the objective coefficient times the retained coordinate is no greater than the right-hand side.

Definition (Lean source)
parameters
n :
ℕ
r :
AugmentedIneq n
x :
Fin n → ℚ
t :
ℚ
def
Holds r x t :
Prop
given by
dotProduct r.coeff x + r.objCoeff * t ≤ r.rhs
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq.Holds · Causalean/Mathlib/Optimization/RationalLP.lean:59 · uses AugmentedIneq
def tail reviewed
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq

Given an augmented rational inequality with one more ordinary coordinate, the tail inequality removes its first ordinary coefficient while retaining its objective coefficient and right-hand side.

Definition (Lean source)
parameters
n :
ℕ
shared
r :
AugmentedIneq (n + 1)
def
tail r :
AugmentedIneq n
given by
clause 1
coeff := Fin.tail r.coeff
clause 2
objCoeff := r.objCoeff
clause 3
rhs := r.rhs
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq.tail · Causalean/Mathlib/Optimization/RationalLP.lean:69 · uses AugmentedIneq
def cancel reviewed
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq

Given two augmented rational inequalities with one more ordinary coordinate, the cancellation inequality has each remaining coefficient, its objective coefficient, and its right-hand side equal to the negative first coefficient of the second inequality times the corresponding quantity of the first, plus the first coefficient of the first inequality times the corresponding quantity of the second.

Definition (Lean source)
parameters
n :
ℕ
shared
p q :
AugmentedIneq (n + 1)
def
cancel p q :
AugmentedIneq n
given by
clause 1
coeff j := (-q.coeff 0) * p.coeff j.succ + p.coeff 0 * q.coeff j.succ
clause 2
objCoeff := (-q.coeff 0) * p.objCoeff + p.coeff 0 * q.objCoeff
clause 3
rhs := (-q.coeff 0) * p.rhs + p.coeff 0 * q.rhs
Causalean.Mathlib.Optimization.RationalLP.AugmentedIneq.cancel · Causalean/Mathlib/Optimization/RationalLP.lean:80 · uses AugmentedIneq
def eliminateOne reviewed
Causalean.Mathlib.Optimization.RationalLP

Given a list of augmented rational inequalities with one more ordinary coordinate, the one-step Fourier--Motzkin elimination output contains the tails of all rows whose first coefficient is zero and, for every row with negative first coefficient and every row with positive first coefficient, their cancellation inequality.

Definition (Lean source)
parameters
n :
ℕ
shared
rows :
List (AugmentedIneq (n + 1))
def
eliminateOne rows :
List (AugmentedIneq n)
given by
(rows.filter (fun r => r.coeff 0 = 0)).map AugmentedIneq.tail ++ (rows.filter (fun r => r.coeff 0 < 0)).flatMap fun q
=> (rows.filter (fun r => 0 < r.coeff 0)).map fun p => p.cancel q
Causalean.Mathlib.Optimization.RationalLP.eliminateOne · Causalean/Mathlib/Optimization/RationalLP.lean:94 · uses AugmentedIneq
def eliminateAll reviewed
Causalean.Mathlib.Optimization.RationalLP

For a nonnegative number of ordinary coordinates and a list of augmented rational inequalities in that many coordinates, the complete Fourier--Motzkin elimination output is the original list when there are no ordinary coordinates and otherwise is obtained by one first-coordinate elimination followed by complete elimination of the remaining coordinates.

Definition (Lean source)
parameters
n :
ℕ
shared
def
eliminateAll n :
(n : ℕ) → List (AugmentedIneq n) → List (AugmentedIneq 0)
given by
clause 1
| 0, rows => rows
clause 2
| n + 1, rows => eliminateAll n (eliminateOne rows)
Causalean.Mathlib.Optimization.RationalLP.eliminateAll · Causalean/Mathlib/Optimization/RationalLP.lean:229 · uses AugmentedIneq
structure Program reviewed
Causalean.Mathlib.Optimization.RationalLP

A rational LP in inequality form: minimize c · x subject to A i · x ≤ b i, with the constraints indexed by an arbitrary type (finiteness is assumed by the algorithms and theorems that need it).

Definition (Lean source)
parameters
ι :
Type*
n :
ℕ
fields
Constraint coefficient rows.
A :
ι → Fin n → ℚ
Constraint right-hand sides.
b :
ι → ℚ
Objective coefficient row.
c :
Fin n → ℚ
Causalean.Mathlib.Optimization.RationalLP.Program · Causalean/Mathlib/Optimization/RationalLP.lean:263
def PrimalFeasible reviewed
Causalean.Mathlib.Optimization.RationalLP.Program

Given a constraint-label set, a number of ordinary variables, a rational linear program, and a rational vector of those variables, the primal-feasibility condition holds exactly when, for every constraint, the dot product of its coefficient row with the vector is no greater than its right-hand side.

Definition (Lean source)
parameters
ι :
Type u_1
shared
n :
ℕ
shared
P :
Program ι n
x :
Fin n → ℚ
i :
def
PrimalFeasible P x :
Prop
given by
dotProduct (P.A i) x ≤ P.b i
Causalean.Mathlib.Optimization.RationalLP.Program.PrimalFeasible · Causalean/Mathlib/Optimization/RationalLP.lean:276 · uses Program
def objective reviewed
Causalean.Mathlib.Optimization.RationalLP.Program

Given a constraint-label set, a number of ordinary variables, a rational linear program, and a rational vector of those variables, the primal objective value is the dot product of the program's objective coefficient vector with that variable vector.

Definition (Lean source)
parameters
ι :
Type u_1
shared
n :
ℕ
shared
P :
Program ι n
x :
Fin n → ℚ
def
objective P x :
ℚ
given by
dotProduct P.c x
Causalean.Mathlib.Optimization.RationalLP.Program.objective · Causalean/Mathlib/Optimization/RationalLP.lean:285 · uses Program
structure CertifiedIneq reviewed
Causalean.Mathlib.Optimization.RationalLP

An augmented inequality together with rational combination weights over a fixed finite family of original rows. The structure does not require the weights to be nonnegative; nonnegativity, which makes the derived row a valid consequence of the original ones, is tracked separately by the elimination construction. The coefficient identity is stated through a common projection of the original variables; this makes repeated elimination independent of coordinate-reassociation bookkeeping.

Definition (Lean source)
parameters
κ :
Type u_2
shared
N :
ℕ
shared
n :
ℕ
shared
base :
κ → AugmentedIneq N
project :
(Fin N → ℚ) → (Fin n → ℚ)
fields
The currently derived inequality.
row :
AugmentedIneq n
Combination weights on the original rows; this structure does not require nonnegativity.
weight :
κ → ℚ
The current coefficient row is the weighted original coefficient row.
coeff_eq :
∀ x, dotProduct row.coeff (project x) = ∑ k, weight k * dotProduct (base k).coeff x
The objective-coordinate coefficient is the same weighted combination.
objCoeff_eq :
row.objCoeff = ∑ k, weight k * (base k).objCoeff
The right-hand side is the same weighted combination.
rhs_eq :
row.rhs = ∑ k, weight k * (base k).rhs
Causalean.Mathlib.Optimization.RationalLP.CertifiedIneq · Causalean/Mathlib/Optimization/RationalLP.lean:443 · uses AugmentedIneq
structure FinalCertifiedIneq reviewed
Causalean.Mathlib.Optimization.RationalLP

A fully eliminated inequality with nonnegative provenance on the original rows and with every original-variable coefficient certified to cancel.

Definition (Lean source)
parameters
κ :
Type u_2
shared
N :
ℕ
shared
base :
κ → AugmentedIneq N
fields
The scalar inequality in the retained objective coordinate.
row :
AugmentedIneq 0
Nonnegative weights on original rows.
weight :
κ → ℚ
Nonnegativity of every original-row weight.
weight_nonneg :
∀ k, 0 ≤ weight k
All original-variable coefficients cancel.
coeff_zero :
∀ x, ∑ k, weight k * dotProduct (base k).coeff x = 0
Objective coefficient combination identity.
objCoeff_eq :
row.objCoeff = ∑ k, weight k * (base k).objCoeff
Right-hand-side combination identity.
rhs_eq :
row.rhs = ∑ k, weight k * (base k).rhs
Causalean.Mathlib.Optimization.RationalLP.FinalCertifiedIneq · Causalean/Mathlib/Optimization/RationalLP.lean:616 · uses AugmentedIneq
def DualFeasible reviewed
Causalean.Mathlib.Optimization.RationalLP.Program

Given a finite set of constraint labels and number of ordinary variables, a finite rational linear program, and rational multipliers for its constraints, the dual-feasibility condition holds exactly when every multiplier is nonnegative and, for every ordinary coordinate, the multiplier-weighted sum of constraint coefficients equals the negative objective coefficient.

Definition (Lean source)
parameters
ι :
Type u_1
shared
n :
ℕ
shared
P :
Program ι n
y :
ι → ℚ
def
DualFeasible P y :
Prop
given by
clause 1
i :
0 ≤ y i
clause 2
j :
∑ i, y i * P.A i j = -P.c j
Causalean.Mathlib.Optimization.RationalLP.Program.DualFeasible · Causalean/Mathlib/Optimization/RationalLP.lean:757 · uses Program
def dualObjective reviewed
Causalean.Mathlib.Optimization.RationalLP.Program

Given a finite set of constraint labels and number of ordinary variables, a finite rational linear program, and rational constraint multipliers, the dual objective value is the negative of the multiplier-weighted sum of the constraint right-hand sides.

Definition (Lean source)
parameters
ι :
Type u_1
shared
n :
ℕ
shared
P :
Program ι n
y :
ι → ℚ
def
dualObjective P y :
ℚ
given by
-(∑ i, y i * P.b i)
Causalean.Mathlib.Optimization.RationalLP.Program.dualObjective · Causalean/Mathlib/Optimization/RationalLP.lean:769 · uses Program
theorem exists_rational_optimal_primal_dual reviewed
Causalean.Mathlib.Optimization.RationalLP

Exact rational LP attainment and strong duality. If a finite rational linear program in inequality form has a feasible rational point and its objective is bounded below on feasible rational points, then it has a rational optimal primal point and rational nonnegative dual multipliers with the same objective value.

Formal statement
hypotheses
ι :
Type u_1
shared
n :
ℕ
shared
P :
Program ι n
hne :
∃ x, P.PrimalFeasible x
hbdd :
∃ l : ℚ, ∀ x, P.PrimalFeasible x → l ≤ P.objective x
conclusion
∃ (xStar : Fin n → ℚ) (yStar : ι → ℚ),
P.PrimalFeasible xStar
P.DualFeasible yStar
P.objective xStar = P.dualObjective yStar
conclusion 1
x :
P.PrimalFeasible x
P.objective xStar ≤ P.objective x
Proof (Lean source)
theorem exists_rational_optimal_primal_dual (P : Program ι n) (hne : ∃ x, P.PrimalFeasible x) (hbdd : ∃ l : ℚ, ∀ x, P.PrimalFeasible x → l ≤ P.objective x) : ∃ (xStar : Fin n → ℚ) (yStar : ι → ℚ), P.PrimalFeasible xStar ∧ P.DualFeasible yStar ∧ P.objective xStar = P.dualObjective yStar ∧ ∀ x, P.PrimalFeasible x → P.objective xStar ≤ P.objective x := by let rows := P.finalCertifiedRows.map FinalCertifiedIneq.row have hrowsne : ∃ t : ℚ, ∀ r ∈ rows, r.Holds elim0 t := by obtain ⟨x, hx⟩ := hne refine ⟨P.objective x, ?_⟩ intro r hr simp only [rows, List.mem_map] at hr obtain ⟨d, hd, rfl⟩ := hr exact (finalCertifiedRows_iff P _).1 ⟨x, hx, rfl⟩ d hd have hrowsbdd : ∃ l : ℚ, ∀ t : ℚ, (∀ r ∈ rows, r.Holds elim0 t) → l ≤ t := by obtain ⟨l, hl⟩ := hbdd refine ⟨l, ?_⟩ intro t ht have hfinal : ∀ d ∈ P.finalCertifiedRows, d.row.Holds elim0 t := by intro d hd exact ht d.row (by change d.row ∈ P.finalCertifiedRows.map FinalCertifiedIneq.row exact List.mem_map.mpr ⟨d, hd, rfl⟩) obtain ⟨x, hx, hxt⟩ := (finalCertifiedRows_iff P t).2 hfinal simpa [← hxt] using hl x hx obtain ⟨v, hvfeas, hvmin, r, hrrows, hrneg, hrv⟩ := scalar_endpoint rows hrowsne hrowsbdd obtain ⟨d, hd, hdr⟩ : ∃ d ∈ P.finalCertifiedRows, d.row = r := by simpa only [rows, List.mem_map] using hrrows subst r obtain ⟨xStar, hxStar, hxval⟩ := (finalCertifiedRows_iff P v).2 (by intro e he exact hvfeas e.row (by change e.row ∈ P.finalCertifiedRows.map FinalCertifiedIneq.row exact List.mem_map.mpr ⟨e, he, rfl⟩)) let denom : ℚ := -d.row.objCoeff have hdenom : 0 < denom := by dsimp [denom]; linarith let yStar : ι → ℚ := fun i => d.weight (.inl i) / denom have hobjcomb : d.row.objCoeff = d.weight (.inr false) - d.weight (.inr true) := by rw [d.objCoeff_eq] simp [Program.certificateBase, Fintype.sum_sum_type, Fintype.sum_bool, sub_eq_add_neg, add_comm] have hcoeff (x : Fin n → ℚ) : (∑ i, d.weight (.inl i) * dotProduct (P.A i) x) - d.weight (.inr false) * dotProduct P.c x + d.weight (.inr true) * dotProduct P.c x = 0 := by have hc0 := d.coeff_zero x simp [Program.certificateBase, Fintype.sum_sum_type, Fintype.sum_bool, neg_dot] at hc0 linarith have hrhs : d.row.rhs = ∑ i, d.weight (.inl i) * P.b i := by rw [d.rhs_eq] simp [Program.certificateBase, Fintype.sum_sum_type, Fintype.sum_bool] refine ⟨xStar, yStar, hxStar, ?_, ?_, ?_⟩ · constructor · intro i exact div_nonneg (d.weight_nonneg (.inl i)) hdenom.le · intro j have hc := hcoeff (fun k => if k = j then 1 else 0) simp only [dotProduct, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, if_true] at hc dsimp [yStar] simp_rw [div_mul_eq_mul_div] rw [← Finset.sum_div] apply (div_eq_iff hdenom.ne').2 dsimp [denom] rw [hobjcomb] ring_nf at hc ⊢ linarith · rw [hxval, ← hrv] dsimp [Program.dualObjective, yStar] simp_rw [div_mul_eq_mul_div] rw [← Finset.sum_div, ← hrhs] dsimp [denom] field_simp · intro x hx rw [hxval] apply hvmin (P.objective x) intro rr hrr simp only [rows, List.mem_map] at hrr obtain ⟨e, he, rfl⟩ := hrr exact (finalCertifiedRows_iff P _).1 ⟨x, hx, rfl⟩ e he
Causalean.Mathlib.Optimization.RationalLP.exists_rational_optimal_primal_dual · Causalean/Mathlib/Optimization/RationalLP.lean:779 · uses Program , DualFeasible , PrimalFeasible , dualObjective , objective
3 supporting declarations (lemmas, instances)
  • eliminateOne_iff theorem — One Fourier–Motzkin elimination step preserves exactly the feasible values of the retained objective coordinate.
    hypotheses
    n :
    ℕ
    List (AugmentedIneq (n + 1))
    Fin n → ℚ
    shared
    t :
    ℚ
    conclusion
    (∃ z : ℚ, ∀ r ∈ rows, r.Holds (cons z x) t) ↔ ∀ r ∈ eliminateOne rows, r.Holds x t
    Proof (Lean source)
    theorem eliminateOne_iff {rows : List (AugmentedIneq (n + 1))} {x : Fin n → ℚ} {t : ℚ} : (∃ z : ℚ, ∀ r ∈ rows, r.Holds (cons z x) t) ↔ ∀ r ∈ eliminateOne rows, r.Holds x t := by constructor · rintro ⟨z, hz⟩ simpa using mem_eliminateOne_of_holds (x := cons z x) hz · exact exists_head_of_eliminateOne
    Causalean.Mathlib.Optimization.RationalLP.eliminateOne_iff · Causalean/Mathlib/Optimization/RationalLP.lean:219
  • eliminateAll_iff theorem — Eliminating all ordinary variables preserves exactly the feasible values of the retained objective coordinate.
    hypotheses
    n :
    ℕ
    List (AugmentedIneq n)
    t :
    ℚ
    conclusion
    (∃ x : Fin n → ℚ, ∀ r ∈ rows, r.Holds x t)
    ↔ ∀ r ∈ eliminateAll n rows, r.Holds elim0 t
    Proof (Lean source)
    theorem eliminateAll_iff {n : ℕ} {rows : List (AugmentedIneq n)} {t : ℚ} : (∃ x : Fin n → ℚ, ∀ r ∈ rows, r.Holds x t) ↔ ∀ r ∈ eliminateAll n rows, r.Holds elim0 t := by induction n with | zero => simp only [eliminateAll] constructor · rintro ⟨x, hx⟩ simpa only [Subsingleton.elim x elim0] using hx · intro hx exact ⟨Fin.elim0, hx⟩ | succ n ih => rw [eliminateAll, ← ih] constructor · rintro ⟨x, hx⟩ exact ⟨Fin.tail x, (eliminateOne_iff.mp ⟨x 0, by simpa using hx⟩)⟩ · rintro ⟨x, hx⟩ obtain ⟨z, hz⟩ := eliminateOne_iff.mpr hx exact ⟨Fin.cons z x, hz⟩
    Causalean.Mathlib.Optimization.RationalLP.eliminateAll_iff · Causalean/Mathlib/Optimization/RationalLP.lean:241
  • exists_rational_primal_optimizer theorem — If a finite rational linear program has a feasible rational point and its objective is bounded below on feasible rational points, then it has a rational primal optimizer.
    hypotheses
    ι :
    Type u_1
    shared
    n :
    ℕ
    shared
    P :
    Program ι n
    hne :
    ∃ x, P.PrimalFeasible x
    hbdd :
    ∃ l : ℚ, ∀ x, P.PrimalFeasible x → l ≤ P.objective x
    conclusion
    ∃ xStar : Fin n → ℚ,
    P.PrimalFeasible xStar
    conclusion 1
    x :
    P.PrimalFeasible x
    P.objective xStar ≤ P.objective x
    Proof (Lean source)
    theorem exists_rational_primal_optimizer (P : Program ι n) (hne : ∃ x, P.PrimalFeasible x) (hbdd : ∃ l : ℚ, ∀ x, P.PrimalFeasible x → l ≤ P.objective x) : ∃ xStar : Fin n → ℚ, P.PrimalFeasible xStar ∧ ∀ x, P.PrimalFeasible x → P.objective xStar ≤ P.objective x := by have hobjne : ∃ t : ℚ, ∀ r ∈ P.objectiveRows, r.Holds elim0 t := by obtain ⟨x, hx⟩ := hne exact ⟨P.objective x, (objectiveRows_iff P _).1 ⟨x, hx, rfl⟩⟩ have hobjbdd : ∃ l : ℚ, ∀ t : ℚ, (∀ r ∈ P.objectiveRows, r.Holds elim0 t) → l ≤ t := by obtain ⟨l, hl⟩ := hbdd refine ⟨l, ?_⟩ intro t ht obtain ⟨x, hx, hxt⟩ := (objectiveRows_iff P t).2 ht simpa [← hxt] using hl x hx obtain ⟨v, hvfeas, hvmin, _⟩ := scalar_endpoint P.objectiveRows hobjne hobjbdd obtain ⟨xStar, hxStar, hxval⟩ := (objectiveRows_iff P v).2 hvfeas refine ⟨xStar, hxStar, ?_⟩ intro x hx rw [hxval] exact hvmin (P.objective x) ((objectiveRows_iff P _).1 ⟨x, hx, rfl⟩)
    Causalean.Mathlib.Optimization.RationalLP.exists_rational_primal_optimizer · Causalean/Mathlib/Optimization/RationalLP.lean:414