Mathlib.Optimization
Optimization helpers staged for Mathlib: weighted-simplex KKT certificates, active-set minimizers, truncation reductions, and boundary-slice selectors.
SimplexActiveSetDefs 5 core · 0 supporting This file contains the shared definitions for the linear-plus-weighted-norm second-order cone program min_{t ∈ Δ_M} Σ αᵢ tᵢ + κ √(Σ βᵢ tᵢ²) over the three-point simplex.
Weighted-simplex active-set SOCP: shared definitions
This file contains the shared definitions for the linear-plus-weighted-norm
second-order cone program
min_{t ∈ Δ_M} Σ αᵢ tᵢ + κ √(Σ βᵢ tᵢ²) over the three-point simplex. It defines
the objective wsObj, simplex membership InSimplex, KKT support data
IsAdmissibleSupport, the induced active-set point activeSetPoint, and the
κ = 0 exposed minimizer face exposedMinFace.
def wsObj reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The weighted-simplex objective Σ αᵢ tᵢ + κ √(Σ βᵢ tᵢ²) in three coordinates (t x, t y, t z) indexed by Fin 3.
def InSimplex reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Membership in the scaled 3-point simplex Δ_M = {t ≥ 0 : Σ tᵢ = M}.
def IsAdmissibleSupport reviewed
⚑ flagged
Causalean.Mathlib.Optimization
KKT-admissible support/multiplier data for the SOCP: a nonempty support S ⊆ {x,y,z} and multiplier λ with Σ_{i∈S} (λ−αᵢ)²/βᵢ = κ², the strict activity λ > αᵢ on S, and the inactivity λ ≤ αⱼ off S.
Definition (Lean source)
def IsAdmissibleSupport (α β : Fin 3 → ℝ) (kappa : ℝ)
(S : Finset (Fin 3)) (lam : ℝ) : Prop :=
S.Nonempty ∧
(∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2 ∧
(∀ i ∈ S, α i < lam) ∧
(∀ j ∉ S, lam ≤ α j)
def activeSetPoint reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The active-set coordinate formula tᵢ = M ((λ−αᵢ)/βᵢ) / Σ_{h∈S} ((λ−αₕ)/βₕ) on S, and tᵢ = 0 off S.
Definition (Lean source)
noncomputable def activeSetPoint (M : ℝ) (α β : Fin 3 → ℝ)
(S : Finset (Fin 3)) (lam : ℝ) : Fin 3 → ℝ :=
fun i => if i ∈ S then
M * ((lam - α i) / β i) / (∑ h ∈ S, (lam - α h) / β h) else 0
def exposedMinFace reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The κ = 0 exposed face conv{M eᵢ : αᵢ = minⱼ αⱼ} of Δ_M: the simplex points supported only on the α-minimizing coordinates.
Definition (Lean source)
def exposedMinFace (M : ℝ) (α : Fin 3 → ℝ) : Set (Fin 3 → ℝ) :=
{ t | InSimplex M t ∧ ∀ i, t i ≠ 0 → ∀ j, α i ≤ α j }
SimplexTruncationDefs 3 core · 0 supporting The parity-truncated simplex K_d, its boundary segment H_d (truncSegPoint), and the endpoint/interior selector s⋆ (truncSelector).
Weighted-simplex truncation: shared definitions
The parity-truncated simplex K_d, its boundary segment H_d (truncSegPoint),
and the endpoint/interior selector s⋆ (truncSelector). Split out of the main
truncation file so both the convexity/reduction helper and the 1-D slice helper can
reference them.
def InTruncSimplex reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Membership in the parity-truncated simplex K_d = {t ∈ Δ_M : t_y + t_z ≥ d}.
Definition (Lean source)
def truncSegPoint reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The boundary segment H_d: the point with t_x = M − d, t_y = s, t_z = d − s.
Definition (Lean source)
def truncSegPoint (M d s : ℝ) : Fin 3 → ℝ := ![M - d, s, d - s]
def truncSelector reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The endpoint/interior selector s⋆ on H_d, with δ = α_y − α_z and A = β_x (M − d)²: s⋆ = 0 if δ ≥ κ d / √(A + d²), s⋆ = d if δ ≤ − κ d / √(A + d²), and otherwise the interior root s⋆ = (d − δ √((A + d²/2)/(κ² − δ²/2)))/2. At κ = 0 the two guards collapse to 0 ≤ δ and δ ≤ 0, recovering the κ = 0 endpoint rule s⋆ = 0 if δ ≥ 0, s⋆ = d if δ ≤ 0.
Definition (Lean source)
noncomputable def truncSelector (M d : ℝ) (α β : Fin 3 → ℝ) (kappa : ℝ) : ℝ :=
let δ := α 1 - α 2
let A := β 0 * (M - d) ^ 2
if kappa * d / sqrt (A + d ^ 2) ≤ δ then 0
else if δ ≤ -(kappa * d / sqrt (A + d ^ 2)) then d
else (d - δ * sqrt ((A + d ^ 2 / 2) / (kappa ^ 2 - δ ^ 2 / 2))) / 2
SimplexActiveSet 1 core · 0 supporting This file packages the active-set/KKT solution of the linear-plus-weighted-norm second-order cone program min_{t ∈ Δ_M} Σ αᵢ tᵢ + κ √(Σ βᵢ tᵢ²) over the three-point simplex. ★ weighted_simplex_active_set
Weighted-simplex active-set SOCP
This file packages the active-set/KKT solution of the linear-plus-weighted-norm
second-order cone program
min_{t ∈ Δ_M} Σ αᵢ tᵢ + κ √(Σ βᵢ tᵢ²) over the three-point simplex. Strict
convexity for κ > 0 gives a unique minimizer, realized by the admissible
support/multiplier pair; for κ = 0, the minimizer set is the exposed
α-minimizing face. The headline theorem is weighted_simplex_active_set.
The shared definitions live in SimplexActiveSetDefs; the analytic content lives
in WeightedSimplexKKT (κ > 0 optimality), WeightedSimplexExists (admissible
support existence), and WeightedSimplexFace (κ = 0 face).
lemma weighted_simplex_active_set reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Weighted-simplex active-set solution. Fix a positive total simplex mass M, linear weights α, coordinate weights β that are all strictly positive, and a nonnegative regularization parameter κ, and consider minimizing the second-order-cone objective Σ αᵢtᵢ + κ·√(Σβᵢtᵢ²) over the three-point simplex Δ_M of total mass M. Then the following two facts hold: whenever κ is strictly positive, there is a unique admissible support/multiplier pair (S, λ), its induced active-set point lies in Δ_M and is the unique global minimizer of the objective, with optimal value the closed form M · λ; and whenever κ equals zero, a point of Δ_M minimizes the objective exactly when it lies on the exposed α-minimizing face. This encodes the displayed KKT coordinate formula, the uniqueness of the admissible support, the value formula, and the κ = 0 face clause.
Formal statement
hypotheses
conclusion
(0 < kappa → ∃! p : Finset (Fin 3) × ℝ, IsAdmissibleSupport α β kappa p.1 p.2 ∧ InSimplex M (activeSetPoint M α β p.1 p.2) ∧ (∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ activeSetPoint M α β p.1 p.2 → wsObj α β kappa (activeSetPoint M α β p.1 p.2) < wsObj α β kappa s) ∧ wsObj α β kappa (activeSetPoint M α β p.1 p.2) = M * p.2) ∧
(kappa = 0 → ∀ t : Fin 3 → ℝ, (InSimplex M t ∧ ∀ s : Fin 3 → ℝ, InSimplex M s → wsObj α β kappa t ≤ wsObj α β kappa s) ↔ t ∈ exposedMinFace M α)
Proof (Lean source)
lemma weighted_simplex_active_set (M : ℝ) (hM : 0 < M)
(α β : Fin 3 → ℝ) (kappa : ℝ)
(hβ : ∀ i, 0 < β i) (hk0 : 0 ≤ kappa) :
(0 < kappa →
∃! p : Finset (Fin 3) × ℝ,
IsAdmissibleSupport α β kappa p.1 p.2 ∧
InSimplex M (activeSetPoint M α β p.1 p.2) ∧
(∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ activeSetPoint M α β p.1 p.2 →
wsObj α β kappa (activeSetPoint M α β p.1 p.2) < wsObj α β kappa s) ∧
wsObj α β kappa (activeSetPoint M α β p.1 p.2) = M * p.2) ∧
(kappa = 0 →
∀ t : Fin 3 → ℝ,
(InSimplex M t ∧
∀ s : Fin 3 → ℝ, InSimplex M s → wsObj α β kappa t ≤ wsObj α β kappa s)
↔ t ∈ exposedMinFace M α) := by
refine ⟨fun hk => ?_, fun hk => ?_⟩
· -- κ > 0: unique admissible pair, active-set point is the strict minimizer, value M·λ.
obtain ⟨S, lam, hadm⟩ := exists_admissible α β kappa hβ hk
refine ⟨(S, lam), ⟨hadm,
activeSetPoint_mem M α β S lam hM.le (fun i _ => hβ i) hadm.1 hadm.2.2.1,
activeSetPoint_strict_min M α β kappa S lam hM hβ hk hadm,
activeSetPoint_value M α β kappa S lam hM.le (fun i _ => hβ i) hk
hadm.1 hadm.2.2.1 hadm.2.1⟩, ?_⟩
rintro ⟨S', lam'⟩ ⟨hadm', hmem', hmin', hval'⟩
-- The two active-set points coincide (each is the strict minimizer of the SOCP).
set t := activeSetPoint M α β S lam with ht
set t' := activeSetPoint M α β S' lam' with ht'
have hmin : ∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ t →
wsObj α β kappa t < wsObj α β kappa s :=
activeSetPoint_strict_min M α β kappa S lam hM hβ hk hadm
have htt' : t = t' := by
by_contra hne
have h1 : wsObj α β kappa t < wsObj α β kappa t' :=
hmin t' (activeSetPoint_mem M α β S' lam' hM.le (fun i _ => hβ i)
hadm'.1 hadm'.2.2.1) (fun h => hne h.symm)
have h2 : wsObj α β kappa t' < wsObj α β kappa t :=
hmin' t (activeSetPoint_mem M α β S lam hM.le (fun i _ => hβ i)
hadm.1 hadm.2.2.1) (fun h => hne h)
exact lt_irrefl _ (h1.trans h2)
-- Supports agree: `i ∈ S ↔ 0 < tᵢ = t'ᵢ ↔ i ∈ S'`.
have hSS' : S = S' := by
ext i
rw [← activeSetPoint_pos_iff M α β S lam hM (fun i _ => hβ i)
hadm.1 hadm.2.2.1 i,
← activeSetPoint_pos_iff M α β S' lam' hM (fun i _ => hβ i)
hadm'.1 hadm'.2.2.1 i, ← ht, ← ht', htt']
-- Multipliers agree via the value formula `M·λ = wsObj t = wsObj t' = M·λ'`.
have hlam : lam = lam' := by
have hv : M * lam = M * lam' := by
rw [← activeSetPoint_value M α β kappa S lam hM.le (fun i _ => hβ i) hk
hadm.1 hadm.2.2.1 hadm.2.1, ← ht, htt', ht',
activeSetPoint_value M α β kappa S' lam' hM.le (fun i _ => hβ i) hk
hadm'.1 hadm'.2.2.1 hadm'.2.1]
exact mul_left_cancel₀ (ne_of_gt hM) hv
exact Prod.ext hSS'.symm hlam.symm
· -- κ = 0: minimizer set is the exposed α-minimizing face.
subst hk
intro t
simpa [wsObj] using kappa_zero_face M α t
SimplexTruncation 2 core · 0 supporting This file packages the constrained minimizer of the weighted-simplex SOCP over the parity-truncated simplex K_d = {t ∈ Δ_M : t_y + t_z ≥ d}. ★ trunc_from_minimizer★ weighted_simplex_truncation
Weighted-simplex truncation
This file packages the constrained minimizer of the weighted-simplex SOCP over
the parity-truncated simplex K_d = {t ∈ Δ_M : t_y + t_z ≥ d}. If the relaxed
optimum over Δ_M is feasible, it is also optimal over K_d; otherwise an
optimum lies on the boundary segment H_d with the explicit endpoint/interior
selector sStar from the 1-D convex slice. The headline theorem is
weighted_simplex_truncation, with trunc_from_minimizer as the reusable
relaxed-minimizer dichotomy.
The definitions (InTruncSimplex, truncSegPoint, truncSelector) live in
SimplexTruncationDefs; the convexity/boundary-reduction step in
SimplexTruncationConvex; the 1-D slice minimization in SimplexTruncationSlice;
and the relaxed-optimum global-minimizer certificates in
SimplexTruncationMinimizers. This file glues them into a single dichotomy
(trunc_from_minimizer) and the headline lemma.
lemma trunc_from_minimizer reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Truncation dichotomy from a relaxed minimizer. Fix a truncation threshold d at most the total simplex mass M, a linear weighting α, coordinate weights β with its zeroth entry nonnegative and its remaining two entries fixed equal to 1, and a nonnegative regularization parameter κ. Given a point t_rel of the simplex Δ_M that globally minimizes the weighted objective wsObj over Δ_M, then the constrained problem over the truncated simplex K_d = {t ∈ Δ_M : t₁ + t₂ ≥ d} splits into two cases: if t_rel already satisfies the truncation constraint, it remains a global minimizer over K_d; otherwise, the face selector point truncSegPoint M d sStar is feasible for K_d and is a global minimizer over K_d. This is the κ-agnostic core shared by the κ > 0 and κ = 0 branches of the headline lemma.
Formal statement
hypotheses
M d :
ℝ
hdM :
d ≤ M
α β :
Fin 3 → ℝ
kappa :
ℝ
hβ0 :
0 ≤ β 0
hβy :
β 1 = 1
hβz :
β 2 = 1
hk :
0 ≤ kappa
t_rel :
Fin 3 → ℝ
hrel :
InSimplex M t_rel
conclusion
(InTruncSimplex M d t_rel → ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) ∧
(¬ (d ≤ t_rel 1 + t_rel 2) → InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧ ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa s)
Proof (Lean source)
lemma trunc_from_minimizer (M d : ℝ) (hdM : d ≤ M)
(α β : Fin 3 → ℝ) (kappa : ℝ)
(hβ0 : 0 ≤ β 0) (hβy : β 1 = 1) (hβz : β 2 = 1) (hk : 0 ≤ kappa)
(t_rel : Fin 3 → ℝ) (hrel : InSimplex M t_rel)
(hmin : ∀ s, InSimplex M s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) :
(InTruncSimplex M d t_rel →
∀ s : Fin 3 → ℝ, InTruncSimplex M d s →
wsObj α β kappa t_rel ≤ wsObj α β kappa s) ∧
(¬ (d ≤ t_rel 1 + t_rel 2) →
InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧
∀ s : Fin 3 → ℝ, InTruncSimplex M d s →
wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa))
≤ wsObj α β kappa s) := by
have hβnn : ∀ i, 0 ≤ β i := by
intro i
fin_cases i
· exact hβ0
· change 0 ≤ β 1
linarith [hβy]
· change 0 ≤ β 2
linarith [hβz]
refine ⟨fun _ s hs => hmin s hs.1, ?_⟩
intro hinf'
have hinf : t_rel 1 + t_rel 2 < d := not_le.mp hinf'
have hdpos : 0 < d := by
have h1 := hrel.1 1; have h2 := hrel.1 2; linarith
obtain ⟨hs0, hsd⟩ := truncSelector_mem M d α β kappa hdpos hβ0 hk
set sStar := truncSelector M d α β kappa with hsStar
have e0 : truncSegPoint M d sStar 0 = M - d := by simp [truncSegPoint]
have e1 : truncSegPoint M d sStar 1 = sStar := by simp [truncSegPoint]
have e2 : truncSegPoint M d sStar 2 = d - sStar := by simp [truncSegPoint]
have n0 : 0 ≤ truncSegPoint M d sStar 0 := by rw [e0]; linarith
have n1 : 0 ≤ truncSegPoint M d sStar 1 := by rw [e1]; linarith
have n2 : 0 ≤ truncSegPoint M d sStar 2 := by rw [e2]; linarith
have hfeas : InTruncSimplex M d (truncSegPoint M d sStar) := by
refine ⟨⟨?_, ?_⟩, ?_⟩
· intro i
fin_cases i
· exact n0
· exact n1
· exact n2
· rw [Fin.sum_univ_three, e0, e1, e2]; ring
· rw [e1, e2]; linarith
refine ⟨hfeas, ?_⟩
intro s hs
obtain ⟨σ, hσ0, hσd, hred⟩ :=
truncSeg_reduction M d kappa α β hβnn hk t_rel hrel hmin hinf s hs
calc wsObj α β kappa (truncSegPoint M d sStar)
≤ wsObj α β kappa (truncSegPoint M d σ) :=
truncSeg_selector_le M d α β kappa hdpos hβ0 hβy hβz hk σ hσ0 hσd
_ ≤ wsObj α β kappa s := hred
lemma weighted_simplex_truncation reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Weighted-simplex truncation. In the notation of weighted_simplex_active_set, fix a positive total simplex mass M, a truncation threshold d at most M, a linear weighting α, coordinate weights β that are everywhere strictly positive with its last two entries fixed equal to 1, and a nonnegative regularization parameter κ. Then the global minimizer of the weighted-simplex objective over the truncated simplex K_d = {t ∈ Δ_M : t₁ + t₂ ≥ d} is given, case by case on the sign of κ, by the active-set/face-selector construction below.
Formal statement
hypotheses
M d :
ℝ
hM :
0 < M
hdM :
d ≤ M
α β :
Fin 3 → ℝ
kappa :
ℝ
hβ :
∀ i, 0 < β i
hβy :
β 1 = 1
hβz :
β 2 = 1
hk :
0 ≤ kappa
conclusion
(0 < kappa → ∀ (S : Finset (Fin 3)) (lam : ℝ), IsAdmissibleSupport α β kappa S lam → (InTruncSimplex M d (activeSetPoint M α β S lam) → ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (activeSetPoint M α β S lam) ≤ wsObj α β kappa s) ∧ (¬ (d ≤ activeSetPoint M α β S lam 1 + activeSetPoint M α β S lam 2) → InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧ ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa s)) ∧
(kappa = 0 → ∀ t_rel : Fin 3 → ℝ, t_rel ∈ exposedMinFace M α → (InTruncSimplex M d t_rel → ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa t_rel ≤ wsObj α β kappa s) ∧ (¬ (d ≤ t_rel 1 + t_rel 2) → InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧ ∀ s : Fin 3 → ℝ, InTruncSimplex M d s → wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa)) ≤ wsObj α β kappa s))
Proof (Lean source)
lemma weighted_simplex_truncation (M d : ℝ) (hM : 0 < M)
(hdM : d ≤ M)
(α β : Fin 3 → ℝ) (kappa : ℝ)
(hβ : ∀ i, 0 < β i)
(hβy : β 1 = 1) (hβz : β 2 = 1) (hk : 0 ≤ kappa) :
(0 < kappa → ∀ (S : Finset (Fin 3)) (lam : ℝ),
IsAdmissibleSupport α β kappa S lam →
(InTruncSimplex M d (activeSetPoint M α β S lam) →
∀ s : Fin 3 → ℝ, InTruncSimplex M d s →
wsObj α β kappa (activeSetPoint M α β S lam) ≤ wsObj α β kappa s) ∧
(¬ (d ≤ activeSetPoint M α β S lam 1 + activeSetPoint M α β S lam 2) →
InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧
∀ s : Fin 3 → ℝ, InTruncSimplex M d s →
wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa))
≤ wsObj α β kappa s)) ∧
(kappa = 0 → ∀ t_rel : Fin 3 → ℝ, t_rel ∈ exposedMinFace M α →
(InTruncSimplex M d t_rel →
∀ s : Fin 3 → ℝ, InTruncSimplex M d s →
wsObj α β kappa t_rel ≤ wsObj α β kappa s) ∧
(¬ (d ≤ t_rel 1 + t_rel 2) →
InTruncSimplex M d (truncSegPoint M d (truncSelector M d α β kappa)) ∧
∀ s : Fin 3 → ℝ, InTruncSimplex M d s →
wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa))
≤ wsObj α β kappa s)) := by
constructor
· -- κ > 0
intro hkpos S lam hadm
obtain ⟨hsimp, hmin⟩ :=
activeSetPoint_isMinimizer M hM α β kappa hβ hkpos S lam hadm
exact trunc_from_minimizer M d hdM α β kappa (hβ 0).le hβy hβz hk _ hsimp hmin
· -- κ = 0
intro hk0 t_rel hface
subst hk0
have hsimp : InSimplex M t_rel := hface.1
have hmin : ∀ s, InSimplex M s → wsObj α β 0 t_rel ≤ wsObj α β 0 s :=
exposedMinFace_isMinimizer M α β t_rel hface
exact trunc_from_minimizer M d hdM α β 0 (hβ 0).le hβy hβz le_rfl _ hsimp hmin
SimplexTruncationConvex 2 core · 2 supporting Two-point convexity of the SOCP objective wsObj (linear term plus a nonnegative multiple of the weighted ℓ² norm), and the geometric consequence that on the truncated simplex K_d any feasible point is dominated in object ★ wsObj_segment_le★ truncSeg_reduction
Weighted-simplex truncation: convexity and boundary reduction
Two-point convexity of the SOCP objective wsObj (linear term plus a nonnegative
multiple of the weighted ℓ² norm), and the geometric consequence that on the
truncated simplex K_d any feasible point is dominated in objective value by a
point of the truncation face H_d, once the relaxed global minimizer is known to
be infeasible (t_rel_y + t_rel_z < d).
lemma wsObj_segment_le reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Two-point convexity of the weighted-simplex objective. For nonnegative coordinate weights β and a nonnegative SOCP scale κ, if θ lies between 0 and 1 then the objective evaluated at the convex combination of two points is at most the same convex combination of the objective values at and at .
Formal statement
Proof (Lean source)
lemma wsObj_segment_le (α β : Fin 3 → ℝ) (kappa : ℝ) (hβ : ∀ i, 0 ≤ β i)
(hk : 0 ≤ kappa) (u v : Fin 3 → ℝ) (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) :
wsObj α β kappa (fun i => (1 - θ) * u i + θ * v i)
≤ (1 - θ) * wsObj α β kappa u + θ * wsObj α β kappa v := by
unfold wsObj
have hlin :
(∑ i, α i * ((1 - θ) * u i + θ * v i))
= (1 - θ) * (∑ i, α i * u i) + θ * (∑ i, α i * v i) := by
repeat rw [Fin.sum_univ_three]
ring
have hsqrt :=
weighted_sqrt_segment_le β hβ u v θ hθ0 hθ1
calc
(∑ i, α i * ((1 - θ) * u i + θ * v i)) +
kappa * sqrt (∑ i, β i * ((1 - θ) * u i + θ * v i) ^ 2)
≤ (1 - θ) * (∑ i, α i * u i) + θ * (∑ i, α i * v i) +
kappa * ((1 - θ) * sqrt (∑ i, β i * u i ^ 2) +
θ * sqrt (∑ i, β i * v i ^ 2)) := by
rw [hlin]
exact add_le_add (le_refl _) (mul_le_mul_of_nonneg_left hsqrt hk)
_ = (1 - θ) * ((∑ i, α i * u i) +
kappa * sqrt (∑ i, β i * u i ^ 2)) +
θ * ((∑ i, α i * v i) +
kappa * sqrt (∑ i, β i * v i ^ 2)) := by
ring
lemma truncSeg_reduction reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Boundary reduction onto the truncation face. Fix nonnegative coordinate weights β and a nonnegative SOCP scale κ. If t_rel lies in the three-coordinate simplex and globally minimizes the objective over that simplex, while t_rel fails the parity cut defining the truncated sub-simplex, since its last two coordinates sum to strictly less than , then for every point t of the truncated sub-simplex , there is some between and such that the boundary point of the truncation face attains an objective value no larger than the objective at t.
Formal statement
hypotheses
M d kappa :
ℝ
α β :
Fin 3 → ℝ
hβ :
∀ i, 0 ≤ β i
hk :
0 ≤ kappa
t_rel :
Fin 3 → ℝ
hrel :
InSimplex M t_rel
hinf :
t_rel 1 + t_rel 2 < d
t :
Fin 3 → ℝ
ht :
InTruncSimplex M d t
conclusion
Proof (Lean source)
lemma truncSeg_reduction (M d kappa : ℝ) (α β : Fin 3 → ℝ)
(hβ : ∀ i, 0 ≤ β i) (hk : 0 ≤ kappa)
(t_rel : Fin 3 → ℝ) (hrel : InSimplex M t_rel)
(hmin : ∀ s, InSimplex M s → wsObj α β kappa t_rel ≤ wsObj α β kappa s)
(hinf : t_rel 1 + t_rel 2 < d)
(t : Fin 3 → ℝ) (ht : InTruncSimplex M d t) :
∃ σ, 0 ≤ σ ∧ σ ≤ d ∧
wsObj α β kappa (truncSegPoint M d σ) ≤ wsObj α β kappa t := by
set S : ℝ := t 1 + t 2
set P : ℝ := t_rel 1 + t_rel 2
have hS_ge : d ≤ S := by
simpa [S] using ht.2
have hP_lt_d : P < d := by simpa [P] using hinf
rcases eq_or_lt_of_le hS_ge with hS_eq | hd_lt_S
· refine ⟨t 1, ht.1.1 1, ?_, ?_⟩
· have ht2 := ht.1.1 2
have hface : t 1 + t 2 = d := by simpa [S] using hS_eq.symm
linarith
· have hface : t 1 + t 2 = d := by simpa [S] using hS_eq.symm
have ht_eq := eq_truncSegPoint_of_simplex_face M d t ht.1 hface
rw [← ht_eq]
· set θ : ℝ := (S - d) / (S - P) with hθ_def
set t_b : Fin 3 → ℝ := fun i => (1 - θ) * t i + θ * t_rel i
have hden_pos : 0 < S - P := by linarith
have hden_ne : S - P ≠ 0 := by linarith
have hθ0 : 0 ≤ θ := by
have hnum : 0 ≤ S - d := by linarith
exact div_nonneg hnum hden_pos.le
have hθmul : θ * (S - P) = S - d := by
rw [hθ_def]
field_simp [hden_ne]
have hθ1 : θ ≤ 1 := by
have hnum_le : S - d ≤ S - P := by linarith
nlinarith
have hθc : 0 ≤ 1 - θ := by linarith
have ht_b12 : t_b 1 + t_b 2 = d := by
simp [t_b]
nlinarith
have ht_b_simplex : InSimplex M t_b := by
refine ⟨?_, ?_⟩
· intro i
have hti := ht.1.1 i
have hri := hrel.1 i
nlinarith [mul_nonneg hθc hti, mul_nonneg hθ0 hri]
· have hsumt := ht.1.2
have hsumr := hrel.2
rw [Fin.sum_univ_three] at hsumt hsumr
rw [Fin.sum_univ_three]
simp [t_b]
nlinarith
refine ⟨t_b 1, ht_b_simplex.1 1, ?_, ?_⟩
· have ht_b2 := ht_b_simplex.1 2
linarith
· have ht_b_eq := eq_truncSegPoint_of_simplex_face M d t_b ht_b_simplex ht_b12
have hconv :
wsObj α β kappa t_b
≤ (1 - θ) * wsObj α β kappa t + θ * wsObj α β kappa t_rel := by
simpa [t_b] using wsObj_segment_le α β kappa hβ hk t t_rel θ hθ0 hθ1
have hrel_le_t : wsObj α β kappa t_rel ≤ wsObj α β kappa t := hmin t ht.1
have hcomb_le :
(1 - θ) * wsObj α β kappa t + θ * wsObj α β kappa t_rel
≤ wsObj α β kappa t := by
nlinarith [mul_le_mul_of_nonneg_left hrel_le_t hθ0]
calc
wsObj α β kappa (truncSegPoint M d (t_b 1)) = wsObj α β kappa t_b := by
rw [← ht_b_eq]
_ ≤ (1 - θ) * wsObj α β kappa t + θ * wsObj α β kappa t_rel := hconv
_ ≤ wsObj α β kappa t := hcomb_le
2 supporting declarations (lemmas, instances)
-
weighted_sqrt_segment_lelemma — The weighted Euclidean root-mean-square of a convex combination is no larger than the same convex combination of the two weighted root-mean-squares.hypothesesProof (Lean source)
lemma weighted_sqrt_segment_le (β : Fin 3 → ℝ) (hβ : ∀ i, 0 ≤ β i) (u v : Fin 3 → ℝ) (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : sqrt (∑ i, β i * ((1 - θ) * u i + θ * v i) ^ 2) ≤ (1 - θ) * sqrt (∑ i, β i * u i ^ 2) + θ * sqrt (∑ i, β i * v i ^ 2) := by have hθc : 0 ≤ 1 - θ := by linarith have hvec : weightedVec β (fun i => (1 - θ) * u i + θ * v i) = (1 - θ) • weightedVec β u + θ • weightedVec β v := by ext i simp [weightedVec] ring calc sqrt (∑ i, β i * ((1 - θ) * u i + θ * v i) ^ 2) = ‖weightedVec β (fun i => (1 - θ) * u i + θ * v i)‖ := by rw [weightedVec_norm β (fun i => (1 - θ) * u i + θ * v i) hβ] _ = ‖(1 - θ) • weightedVec β u + θ • weightedVec β v‖ := by rw [hvec] _ ≤ ‖(1 - θ) • weightedVec β u‖ + ‖θ • weightedVec β v‖ := norm_add_le _ _ _ = (1 - θ) * sqrt (∑ i, β i * u i ^ 2) + θ * sqrt (∑ i, β i * v i ^ 2) := by rw [norm_smul, norm_smul, weightedVec_norm β u hβ, weightedVec_norm β v hβ] simp [Real.norm_eq_abs, abs_of_nonneg hθc, abs_of_nonneg hθ0] -
eq_truncSegPoint_of_simplex_facelemma — A three-coordinate vector with total mass M whose last two coordinates sum to d is the corresponding point on the truncation segment, indexed by its second coordinate.hypothesesconclusionx = truncSegPoint M d (x 1)Proof (Lean source)
lemma eq_truncSegPoint_of_simplex_face (M d : ℝ) (x : Fin 3 → ℝ) (hx : InSimplex M x) (hxd : x 1 + x 2 = d) : x = truncSegPoint M d (x 1) := by funext i fin_cases i · have hsum := hx.2 rw [Fin.sum_univ_three] at hsum simp [truncSegPoint] linarith · simp [truncSegPoint] · simp [truncSegPoint] linarith
SimplexTruncationMinimizers 2 core · 0 supporting Self-contained proofs that the two relaxed-optimum descriptions used by the truncation lemma really are global minimizers of wsObj over the full simplex Δ_M, so the truncation argument does not depend on weighted_simplex ★ activeSetPoint_isMinimizer★ exposedMinFace_isMinimizer
Weighted-simplex truncation: relaxed global minimizers
Self-contained proofs that the two relaxed-optimum descriptions used by the
truncation lemma really are global minimizers of wsObj over the full simplex
Δ_M, so the truncation argument does not depend on weighted_simplex_active_set:
* activeSetPoint_isMinimizer (κ > 0): any KKT-admissible support/multiplier pair
induces a simplex point that globally minimizes wsObj. The optimality is a
Cauchy–Schwarz (weighted ℓ²) certificate: κ β_i t*_i / ‖t*‖_β = λ − α_i on the
support and α_j ≥ λ off it, so the first-order (subgradient) inequality collapses
to λ·(Σ s − M) = 0.
* exposedMinFace_isMinimizer (κ = 0): a point of the exposed α-minimizing face
minimizes the (now purely linear) objective, since its mass sits on argmin α.
lemma activeSetPoint_isMinimizer reviewed
⚑ flagged
Causalean.Mathlib.Optimization
KKT admissible ⟹ global minimizer (κ > 0). For a positive total mass M, positive coordinate weights β, a positive SOCP scale κ, and a KKT-admissible support/multiplier pair (S, λ): a nonempty index set S with , strict activity on S, and inactivity off S, the induced active-set point lies in the simplex and globally minimizes the objective over that simplex.
Formal statement
hypotheses
M :
ℝ
hM :
0 < M
α β :
Fin 3 → ℝ
kappa :
ℝ
hβ :
∀ i, 0 < β i
hkpos :
0 < kappa
lam :
ℝ
hadm :
IsAdmissibleSupport α β kappa S lam
conclusion
InSimplex M (activeSetPoint M α β S lam) ∧
∀ s : Fin 3 → ℝ,
Proof (Lean source)
lemma activeSetPoint_isMinimizer (M : ℝ) (hM : 0 < M) (α β : Fin 3 → ℝ) (kappa : ℝ)
(hβ : ∀ i, 0 < β i) (hkpos : 0 < kappa)
(S : Finset (Fin 3)) (lam : ℝ) (hadm : IsAdmissibleSupport α β kappa S lam) :
InSimplex M (activeSetPoint M α β S lam) ∧
∀ s : Fin 3 → ℝ, InSimplex M s →
wsObj α β kappa (activeSetPoint M α β S lam) ≤ wsObj α β kappa s := by
classical
rcases hadm with ⟨hSne, hsum, hact, hoff⟩
let t : Fin 3 → ℝ := activeSetPoint M α β S lam
let D : ℝ := ∑ h ∈ S, (lam - α h) / β h
have hDpos : 0 < D := by
dsimp [D]
exact Finset.sum_pos
(fun i hi => div_pos (sub_pos.mpr (hact i hi)) (hβ i)) hSne
have htS : ∀ i, i ∈ S → t i = M * ((lam - α i) / β i) / D := by
intro i hi
simp [t, activeSetPoint, hi, D]
have htOff : ∀ i, i ∉ S → t i = 0 := by
intro i hi
simp [t, activeSetPoint, hi]
have htpos : ∀ i, i ∈ S → 0 < t i := by
intro i hi
rw [htS i hi]
exact div_pos (mul_pos hM (div_pos (sub_pos.mpr (hact i hi)) (hβ i))) hDpos
have ht_nonneg : ∀ i, 0 ≤ t i := by
intro i
by_cases hi : i ∈ S
· exact (htpos i hi).le
· rw [htOff i hi]
have hsum_t_support :
(∑ i, t i) = ∑ i ∈ S, M * ((lam - α i) / β i) / D := by
calc
(∑ i, t i) = ∑ i, if i ∈ S then M * ((lam - α i) / β i) / D else 0 := by
apply Finset.sum_congr rfl
intro i _
by_cases hi : i ∈ S
· simp [hi, htS i hi]
· simp [hi, htOff i hi]
_ = ∑ i ∈ S, M * ((lam - α i) / β i) / D := by
simp
have hsum_t : ∑ i, t i = M := by
rw [hsum_t_support]
calc
(∑ i ∈ S, M * ((lam - α i) / β i) / D)
= ∑ i ∈ S, (M / D) * ((lam - α i) / β i) := by
apply Finset.sum_congr rfl
intro i _
field_simp [hDpos.ne']
_ = (M / D) * ∑ i ∈ S, (lam - α i) / β i := by
rw [Finset.mul_sum]
_ = (M / D) * D := by
rfl
_ = M := by
field_simp [hDpos.ne']
have ht_simplex : InSimplex M t := ⟨ht_nonneg, hsum_t⟩
refine ⟨ht_simplex, ?_⟩
intro s hs
let Nt : ℝ := sqrt (∑ i, β i * t i ^ 2)
let Ns : ℝ := sqrt (∑ i, β i * s i ^ 2)
have ht_sq_nonneg : 0 ≤ ∑ i, β i * t i ^ 2 := by
exact sum_nonneg (fun i _ => mul_nonneg (hβ i).le (sq_nonneg (t i)))
have hs_sq_nonneg : 0 ≤ ∑ i, β i * s i ^ 2 := by
exact sum_nonneg (fun i _ => mul_nonneg (hβ i).le (sq_nonneg (s i)))
have hNt_sq : Nt ^ 2 = ∑ i, β i * t i ^ 2 := by
dsimp [Nt]
rw [Real.sq_sqrt ht_sq_nonneg]
have hNs_sq : Ns ^ 2 = ∑ i, β i * s i ^ 2 := by
dsimp [Ns]
rw [Real.sq_sqrt hs_sq_nonneg]
have hquad_support :
(∑ i, β i * t i ^ 2) =
∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2 := by
calc
(∑ i, β i * t i ^ 2) =
∑ i, if i ∈ S then β i * (M * ((lam - α i) / β i) / D) ^ 2 else 0 := by
apply Finset.sum_congr rfl
intro i _
by_cases hi : i ∈ S
· simp [hi, htS i hi]
· simp [hi, htOff i hi]
_ = ∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2 := by
simp
have hquad :
(∑ i, β i * t i ^ 2) = M ^ 2 * kappa ^ 2 / D ^ 2 := by
rw [hquad_support]
calc
(∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2)
= ∑ i ∈ S, (M ^ 2 / D ^ 2) * ((lam - α i) ^ 2 / β i) := by
apply Finset.sum_congr rfl
intro i _
field_simp [(hβ i).ne', hDpos.ne']
_ = (M ^ 2 / D ^ 2) * ∑ i ∈ S, (lam - α i) ^ 2 / β i := by
rw [Finset.mul_sum]
_ = (M ^ 2 / D ^ 2) * kappa ^ 2 := by
rw [hsum]
_ = M ^ 2 * kappa ^ 2 / D ^ 2 := by
field_simp [hDpos.ne']
have hNt_nonneg : 0 ≤ Nt := by
dsimp [Nt]
exact Real.sqrt_nonneg _
have hNt_formula : Nt = M * kappa / D := by
have hright_nonneg : 0 ≤ M * kappa / D := by positivity
apply (Real.sqrt_eq_iff_mul_self_eq ht_sq_nonneg hright_nonneg).2
rw [hquad]
field_simp [hDpos.ne']
have hNtpos : 0 < Nt := by
rw [hNt_formula]
positivity
have hcoord : ∀ i, i ∈ S → kappa * (β i * t i) = (lam - α i) * Nt := by
intro i hi
rw [htS i hi, hNt_formula]
field_simp [(hβ i).ne', hDpos.ne']
have hCS : (∑ i, β i * t i * s i) ≤ Nt * Ns := by
exact (le_abs_self _).trans (by
simpa [Nt, Ns, mul_assoc] using
abs_weighted_inner_le
(Finset.univ : Finset (Fin 3)) β t s (fun i _ => (hβ i).le))
have hcross_eq : ∀ y : Fin 3 → ℝ,
kappa * (∑ i, β i * t i * y i) =
Nt * ∑ i ∈ S, (lam - α i) * y i := by
intro y
calc
kappa * (∑ i, β i * t i * y i)
= ∑ i, (kappa * (β i * t i)) * y i := by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro i _
ring
_ = ∑ i, if i ∈ S then ((lam - α i) * Nt) * y i else 0 := by
apply Finset.sum_congr rfl
intro i _
by_cases hi : i ∈ S
· simp [hi, hcoord i hi]
· simp [hi, htOff i hi]
_ = ∑ i ∈ S, ((lam - α i) * Nt) * y i := by
simp
_ = Nt * ∑ i ∈ S, (lam - α i) * y i := by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro i _
ring
have hsupport_s_bound : (∑ i ∈ S, (lam - α i) * s i) ≤ kappa * Ns := by
have hmul := mul_le_mul_of_nonneg_left hCS hkpos.le
rw [hcross_eq s] at hmul
have hmul' : Nt * (∑ i ∈ S, (lam - α i) * s i) ≤ Nt * (kappa * Ns) := by
simpa [mul_assoc, mul_left_comm, mul_comm] using hmul
exact le_of_mul_le_mul_left hmul' hNtpos
have hcross_tt : (∑ i, β i * t i * t i) = Nt ^ 2 := by
calc
(∑ i, β i * t i * t i) = ∑ i, β i * t i ^ 2 := by
apply Finset.sum_congr rfl
intro i _
ring
_ = Nt ^ 2 := hNt_sq.symm
have hsupport_t_eq : (∑ i ∈ S, (lam - α i) * t i) = kappa * Nt := by
have h := hcross_eq t
rw [hcross_tt] at h
have h' : Nt * (∑ i ∈ S, (lam - α i) * t i) = Nt * (kappa * Nt) := by
calc
Nt * (∑ i ∈ S, (lam - α i) * t i) = kappa * Nt ^ 2 := h.symm
_ = Nt * (kappa * Nt) := by ring
exact mul_left_cancel₀ hNtpos.ne' h'
have hsum_t_compl : (∑ i ∈ Sᶜ, t i) = 0 := by
apply Finset.sum_eq_zero
intro i hi
exact htOff i (by simpa using hi)
have hsum_t_S : (∑ i ∈ S, t i) = M := by
calc
(∑ i ∈ S, t i) = (∑ i, t i) := by
rw [← Finset.sum_add_sum_compl S t, hsum_t_compl, add_zero]
_ = M := hsum_t
have halpha_t_compl : (∑ i ∈ Sᶜ, α i * t i) = 0 := by
apply Finset.sum_eq_zero
intro i hi
simp [htOff i (by simpa using hi)]
have halpha_t_support : (∑ i, α i * t i) = ∑ i ∈ S, α i * t i := by
rw [← Finset.sum_add_sum_compl S (fun i => α i * t i), halpha_t_compl, add_zero]
have hvalue_t : wsObj α β kappa t = lam * M := by
calc
wsObj α β kappa t = (∑ i, α i * t i) + kappa * Nt := by
simp [wsObj, Nt]
_ = (∑ i ∈ S, α i * t i) + ∑ i ∈ S, (lam - α i) * t i := by
rw [halpha_t_support, hsupport_t_eq]
_ = ∑ i ∈ S, lam * t i := by
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro i _
ring
_ = lam * ∑ i ∈ S, t i := by
rw [Finset.mul_sum]
_ = lam * M := by
rw [hsum_t_S]
have hoff_s_bound : (∑ i ∈ Sᶜ, lam * s i) ≤ ∑ i ∈ Sᶜ, α i * s i := by
apply Finset.sum_le_sum
intro i hi
exact mul_le_mul_of_nonneg_right (hoff i (by simpa using hi)) (hs.1 i)
have hlinear_s_bound :
lam * M ≤ (∑ i, α i * s i) + ∑ i ∈ S, (lam - α i) * s i := by
have hsplit_lam := Finset.sum_add_sum_compl S (fun i => lam * s i)
have hsplit_alpha := Finset.sum_add_sum_compl S (fun i => α i * s i)
have hactive :
(∑ i ∈ S, α i * s i) + ∑ i ∈ S, (lam - α i) * s i =
∑ i ∈ S, lam * s i := by
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro i _
ring
have hfull_lam : (∑ i, lam * s i) = lam * M := by
calc
(∑ i, lam * s i) = lam * ∑ i, s i := by
rw [Finset.mul_sum]
_ = lam * M := by
rw [hs.2]
calc
lam * M = ∑ i, lam * s i := hfull_lam.symm
_ = (∑ i ∈ S, lam * s i) + ∑ i ∈ Sᶜ, lam * s i := hsplit_lam.symm
_ ≤ (∑ i ∈ S, lam * s i) + ∑ i ∈ Sᶜ, α i * s i := by
simpa [add_comm, add_left_comm, add_assoc] using
add_le_add_left hoff_s_bound (∑ i ∈ S, lam * s i)
_ = (∑ i, α i * s i) + ∑ i ∈ S, (lam - α i) * s i := by
rw [← hactive, ← hsplit_alpha]
ring
have hvalue_s : lam * M ≤ wsObj α β kappa s := by
calc
lam * M ≤ (∑ i, α i * s i) + ∑ i ∈ S, (lam - α i) * s i :=
hlinear_s_bound
_ ≤ (∑ i, α i * s i) + kappa * Ns := by
simpa [add_comm, add_left_comm, add_assoc] using
add_le_add_left hsupport_s_bound (∑ i, α i * s i)
_ = wsObj α β kappa s := by
simp [wsObj, Ns]
calc
wsObj α β kappa (activeSetPoint M α β S lam) = wsObj α β kappa t := by
simp [t]
_ = lam * M := hvalue_t
_ ≤ wsObj α β kappa s := hvalue_s
lemma exposedMinFace_isMinimizer reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Exposed face ⟹ global minimizer (κ = 0). If t_rel lies in the simplex and every coordinate at which it is nonzero attains the minimum value of α, then t_rel globally minimizes the purely linear objective — wsObj at — over the whole simplex.
Formal statement
Proof (Lean source)
lemma exposedMinFace_isMinimizer (M : ℝ) (α β : Fin 3 → ℝ)
(t_rel : Fin 3 → ℝ) (hface : t_rel ∈ exposedMinFace M α) :
∀ s : Fin 3 → ℝ, InSimplex M s →
wsObj α β 0 t_rel ≤ wsObj α β 0 s := by
simpa [wsObj] using ((kappa_zero_face M α t_rel).2 hface).2
SimplexTruncationSlice 2 core · 4 supporting On the truncation face H_d the objective restricts to the 1-D convex function g_d(σ) = α_x(M−d) + α_y σ + α_z(d−σ) + κ √(A + σ² + (d−σ)²), with A = β_x(M−d)². ★ wsObj_truncSeg_eq★ truncSeg_selector_le
Weighted-simplex truncation: the 1-D boundary slice
On the truncation face H_d the objective restricts to the 1-D convex function
g_d(σ) = α_x(M−d) + α_y σ + α_z(d−σ) + κ √(A + σ² + (d−σ)²), with A = β_x(M−d)².
This file computes that restriction (wsObj_truncSeg_eq), shows the selector s⋆
lands in [0,d] (truncSelector_mem), and proves g_d is minimized at s⋆
(truncSeg_selector_le) via the tangent-line inequality of the convex slice.
lemma wsObj_truncSeg_eq reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Objective on the truncation face. For a total budget M and a truncation level d, a linear weight vector α and a quadratic weight vector β, and a curvature coefficient kappa and a face coordinate σ, evaluating the weighted-simplex objective at the truncation-face point (M−d, σ, d−σ) gives the explicit one-dimensional form α₀(M−d) + α₁σ + α₂(d−σ) + κ√(β₀(M−d)² + β₁σ² + β₂(d−σ)²).
Formal statement
hypotheses
conclusion
wsObj α β kappa (truncSegPoint M d σ)
= α 0 * (M - d)
+ α 1 * σ
+ α 2 * (d - σ)
+ kappa * sqrt (β 0 * (M - d) ^ 2 + β 1 * σ ^ 2 + β 2 * (d - σ) ^ 2)
Proof (Lean source)
lemma wsObj_truncSeg_eq (M d : ℝ) (α β : Fin 3 → ℝ) (kappa σ : ℝ)
:
wsObj α β kappa (truncSegPoint M d σ)
= α 0 * (M - d) + α 1 * σ + α 2 * (d - σ)
+ kappa * sqrt
(β 0 * (M - d) ^ 2 + β 1 * σ ^ 2 + β 2 * (d - σ) ^ 2) := by
unfold wsObj truncSegPoint
rw [Fin.sum_univ_three, Fin.sum_univ_three]
simp [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two]
lemma truncSeg_selector_le reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The selector minimizes the boundary slice. Suppose the truncation width is positive, the first-coordinate weight is nonnegative while the other two weights both equal 1, and the SOCP scale is nonnegative. Then for every offset between and , the objective wsObj evaluated at the boundary point truncSegPoint M d applied to the selector truncSelector M d α β κ is at most its value at the boundary point for .
Formal statement
hypotheses
M d :
ℝ
α β :
Fin 3 → ℝ
kappa :
ℝ
hd :
0 < d
hβ0 :
0 ≤ β 0
hβy :
β 1 = 1
hβz :
β 2 = 1
hk :
0 ≤ kappa
σ :
ℝ
hσ0 :
0 ≤ σ
hσd :
σ ≤ d
conclusion
≤ wsObj α β kappa (truncSegPoint M d σ)
Proof (Lean source)
lemma truncSeg_selector_le (M d : ℝ) (α β : Fin 3 → ℝ) (kappa : ℝ)
(hd : 0 < d) (hβ0 : 0 ≤ β 0) (hβy : β 1 = 1) (hβz : β 2 = 1) (hk : 0 ≤ kappa)
(σ : ℝ) (hσ0 : 0 ≤ σ) (hσd : σ ≤ d) :
wsObj α β kappa (truncSegPoint M d (truncSelector M d α β kappa))
≤ wsObj α β kappa (truncSegPoint M d σ) := by
set s := truncSelector M d α β kappa with hs
rw [wsObj_truncSeg_eq M d α β kappa s, wsObj_truncSeg_eq M d α β kappa σ]
simp only [hβy, hβz, one_mul]
set A := β 0 * (M - d) ^ 2 with hAdef
set δ := α 1 - α 2 with hδdef
let Rs := A + s ^ 2 + (d - s) ^ 2
let Rσ := A + σ ^ 2 + (d - σ) ^ 2
let rs := Real.sqrt Rs
let rσ := Real.sqrt Rσ
have hA : 0 ≤ A := by
dsimp [A]
exact mul_nonneg hβ0 (sq_nonneg _)
have hRs_pos : 0 < Rs := by
dsimp [Rs]
exact truncSeg_radicand_pos hA hd
have hRσ_pos : 0 < Rσ := by
dsimp [Rσ]
exact truncSeg_radicand_pos hA hd
have hrs_pos : 0 < rs := by
exact Real.sqrt_pos.2 hRs_pos
have hrs_sq : rs ^ 2 = Rs := by
simp [rs, Real.sq_sqrt (le_of_lt hRs_pos)]
have hCS :
A + s * σ + (d - s) * (d - σ) ≤ rs * rσ := by
simpa [rs, rσ, Rs, Rσ] using
truncSeg_cs_sqrt (A := A) (d := d) (s := s) (σ := σ) hA
have hcross_id :
A + s * σ + (d - s) * (d - σ) - Rs =
(σ - s) * (2 * s - d) := by
dsimp [Rs]
ring
have hdiff :
(σ - s) * (2 * s - d) ≤ rs * rσ - rs * rs := by
nlinarith [hCS, hcross_id, hrs_sq]
have hkdiff :
kappa * ((σ - s) * (2 * s - d)) ≤
kappa * (rs * rσ - rs * rs) :=
mul_le_mul_of_nonneg_left hdiff hk
have hs_core :
s =
if kappa * d / Real.sqrt (A + d ^ 2) ≤ δ then 0
else if δ ≤ -(kappa * d / Real.sqrt (A + d ^ 2)) then d
else (d - δ *
Real.sqrt ((A + d ^ 2 / 2) / (kappa ^ 2 - δ ^ 2 / 2))) / 2 := by
rw [hs]
simp [truncSelector, A, δ]
have hsign :
0 ≤ (σ - s) * (rs * δ + kappa * (2 * s - d)) := by
have hsign_core :=
truncSelector_sign_core (A := A) (d := d) (kappa := kappa)
(δ := δ) (σ := σ) hd hA hk hσ0 hσd
dsimp only at hsign_core
rw [← hs_core] at hsign_core
simpa [rs, Rs] using hsign_core
have hmul_nonneg :
0 ≤ rs * (δ * (σ - s) + kappa * (rσ - rs)) := by
nlinarith [hsign, hkdiff]
have hnonneg : 0 ≤ δ * (σ - s) + kappa * (rσ - rs) := by
have hmul' :
0 ≤ (δ * (σ - s) + kappa * (rσ - rs)) * rs := by
simpa [mul_comm, mul_left_comm, mul_assoc] using hmul_nonneg
exact nonneg_of_mul_nonneg_left hmul' hrs_pos
have hslice_delta : δ * s + kappa * rs ≤ δ * σ + kappa * rσ := by
nlinarith
have hslice :
α 1 * s + α 2 * (d - s) + kappa * rs ≤
α 1 * σ + α 2 * (d - σ) + kappa * rσ := by
nlinarith [hslice_delta]
dsimp [rs, rσ, Rs, Rσ, A]
nlinarith [hslice]
4 supporting declarations (lemmas, instances)
-
truncSeg_cs_sqrtlemma — For a nonnegative baseline component, the inner product of two three-dimensional boundary vectors is no greater than the product of their Euclidean norms.hypothesesA d s σ :ℝhA :0 ≤ AProof (Lean source)
lemma truncSeg_cs_sqrt {A d s σ : ℝ} (hA : 0 ≤ A) : A + s * σ + (d - s) * (d - σ) ≤ Real.sqrt (A + s ^ 2 + (d - s) ^ 2) * Real.sqrt (A + σ ^ 2 + (d - σ) ^ 2) := by set a := Real.sqrt A have ha2 : a ^ 2 = A := by simp [a, Real.sq_sqrt hA] have hsq : (A + s * σ + (d - s) * (d - σ)) ^ 2 ≤ (A + s ^ 2 + (d - s) ^ 2) * (A + σ ^ 2 + (d - σ) ^ 2) := by have hid : (A + s ^ 2 + (d - s) ^ 2) * (A + σ ^ 2 + (d - σ) ^ 2) - (A + s * σ + (d - s) * (d - σ)) ^ 2 = (a * σ - s * a) ^ 2 + (a * (d - σ) - (d - s) * a) ^ 2 + (s * (d - σ) - (d - s) * σ) ^ 2 := by rw [← ha2] ring nlinarith [hid, sq_nonneg (a * σ - s * a), sq_nonneg (a * (d - σ) - (d - s) * a), sq_nonneg (s * (d - σ) - (d - s) * σ)] have hX : 0 ≤ A + s ^ 2 + (d - s) ^ 2 := truncSeg_radicand_nonneg hA have hY : 0 ≤ A + σ ^ 2 + (d - σ) ^ 2 := truncSeg_radicand_nonneg hA calc A + s * σ + (d - s) * (d - σ) ≤ |A + s * σ + (d - s) * (d - σ)| := le_abs_self _ _ ≤ Real.sqrt ((A + s ^ 2 + (d - s) ^ 2) * (A + σ ^ 2 + (d - σ) ^ 2)) := by exact Real.le_sqrt_of_sq_le (by simpa [sq_abs] using hsq) _ = Real.sqrt (A + s ^ 2 + (d - s) ^ 2) * Real.sqrt (A + σ ^ 2 + (d - σ) ^ 2) := by rw [Real.sqrt_mul hX] -
truncSelector_interior_sq_boundlemma — If the truncation offset lies strictly between the two interior guard bounds, then its squared size times the radicand is strictly smaller than the squared truncation scale times the squared interval width.hypothesesA d kappa δ :ℝhd :0 < dhA :0 ≤ Ahk :0 ≤ kappahlo :¬ kappa * d / sqrt (A + d ^ 2) ≤ δhhi :¬ δ ≤ -(kappa * d / sqrt (A + d ^ 2))conclusionδ ^ 2 * (A + d ^ 2) < kappa ^ 2 * d ^ 2Proof (Lean source)
lemma truncSelector_interior_sq_bound {A d kappa δ : ℝ} (hd : 0 < d) (hA : 0 ≤ A) (hk : 0 ≤ kappa) (hlo : ¬ kappa * d / sqrt (A + d ^ 2) ≤ δ) (hhi : ¬ δ ≤ -(kappa * d / sqrt (A + d ^ 2))) : δ ^ 2 * (A + d ^ 2) < kappa ^ 2 * d ^ 2 := by have hrad_pos : 0 < A + d ^ 2 := by nlinarith [hA, sq_pos_of_pos hd] have hBpos : 0 < sqrt (A + d ^ 2) := Real.sqrt_pos.2 hrad_pos have hBsq : sqrt (A + d ^ 2) ^ 2 = A + d ^ 2 := Real.sq_sqrt (le_of_lt hrad_pos) have hlt : δ < kappa * d / sqrt (A + d ^ 2) := lt_of_not_ge hlo have hgt : -(kappa * d / sqrt (A + d ^ 2)) < δ := lt_of_not_ge hhi have h_abs : |δ| < kappa * d / sqrt (A + d ^ 2) := by rw [abs_lt] exact ⟨hgt, hlt⟩ have hright_nonneg : 0 ≤ kappa * d / sqrt (A + d ^ 2) := by positivity have h_abs_abs : |δ| < |kappa * d / sqrt (A + d ^ 2)| := by rwa [abs_of_nonneg hright_nonneg] have hsquare := sq_lt_sq.mpr h_abs_abs field_simp [ne_of_gt hBpos] at hsquare nlinarith [hBsq, hsquare] -
truncSelector_interior_den_poslemma — Under the selector's strict interior guard inequalities, a positive interval width, and nonnegative baseline and scale, the squared-scale denominator minus half the squared offset is positive.hypothesesA d kappa δ :ℝhd :0 < dhA :0 ≤ Ahk :0 ≤ kappahlo :¬ kappa * d / sqrt (A + d ^ 2) ≤ δhhi :¬ δ ≤ -(kappa * d / sqrt (A + d ^ 2))conclusion0 < kappa ^ 2 - δ ^ 2 / 2Proof (Lean source)
lemma truncSelector_interior_den_pos {A d kappa δ : ℝ} (hd : 0 < d) (hA : 0 ≤ A) (hk : 0 ≤ kappa) (hlo : ¬ kappa * d / sqrt (A + d ^ 2) ≤ δ) (hhi : ¬ δ ≤ -(kappa * d / sqrt (A + d ^ 2))) : 0 < kappa ^ 2 - δ ^ 2 / 2 := by have hsq_lt : δ ^ 2 * (A + d ^ 2) < kappa ^ 2 * d ^ 2 := truncSelector_interior_sq_bound hd hA hk hlo hhi have hd2pos : 0 < d ^ 2 := sq_pos_of_pos hd have hratio_le : d ^ 2 ≤ A + d ^ 2 := by nlinarith [hA] have hden_half : δ ^ 2 / 2 < kappa ^ 2 := by nlinarith [hsq_lt, hratio_le, hd2pos] nlinarith -
truncSelector_memlemma — The selector lands in [0,d]. The endpoint/interior selector truncSelector satisfies 0 ≤ s⋆ ≤ d: the two endpoint branches give 0 and d directly, and in the interior branch the guard failures |δ| < κ d / √(A + d²) force δ²(A + d²) < κ² d², whence |s⋆ − d/2| < d/2.hypothesesconclusion0 ≤ truncSelector M d α β kappa ∧ truncSelector M d α β kappa ≤ dProof (Lean source)
lemma truncSelector_mem (M d : ℝ) (α β : Fin 3 → ℝ) (kappa : ℝ) (hd : 0 < d) (hβ0 : 0 ≤ β 0) (hk : 0 ≤ kappa) : 0 ≤ truncSelector M d α β kappa ∧ truncSelector M d α β kappa ≤ d := by unfold truncSelector let δ := α 1 - α 2 let A := β 0 * (M - d) ^ 2 have hA : 0 ≤ A := by dsimp [A] exact mul_nonneg hβ0 (sq_nonneg _) dsimp only split_ifs with hlo hhi · exact ⟨le_rfl, le_of_lt hd⟩ · exact ⟨le_of_lt hd, le_rfl⟩ · exact truncSelector_interior_mem hd hA hk hlo hhi
WeightedSimplexCS 2 core · 0 supporting Cauchy–Schwarz for the weighted inner product ⟨s,t⟩_β = Σ βᵢ sᵢ tᵢ on a finite index type, in the squared form weighted_cs_sq and the strict simplex-slice form weighted_cs_simplex_strict. ★ weighted_cs_sq★ weighted_cs_simplex_strict
Weighted Cauchy–Schwarz on the three-point simplex
Cauchy–Schwarz for the weighted inner product ⟨s,t⟩_β = Σ βᵢ sᵢ tᵢ on a finite index type,
in the squared form weighted_cs_sq and the strict simplex-slice form
weighted_cs_simplex_strict. The strict version is used to prove uniqueness for
the weighted-simplex SOCP: on the affine slice Σ sᵢ = Σ tᵢ = M > 0, distinct
points are not positive scalar multiples of each other, so equality in
Cauchy–Schwarz cannot occur.
The squared form is the arbitrary-finite-index
Causalean.Mathlib.Analysis.weighted_inner_sq_le; only the strict version is genuinely
three-dimensional (its proof uses the explicit Lagrange identity).
lemma weighted_cs_sq reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Weighted Cauchy–Schwarz (squared form). For finitely many coordinates weighted by nonnegative masses β, the square of the weighted inner product of two vectors and is at most the product of their weighted sums of squares .
Formal statement
hypotheses
conclusion
(∑ i, β i * (s i * t i)) ^ 2 ≤ (∑ i, β i * s i ^ 2) * (∑ i, β i * t i ^ 2)
Proof (Lean source)
lemma weighted_cs_sq {ι : Type*} [Fintype ι] (β s t : ι → ℝ) (hβ : ∀ i, 0 ≤ β i) :
(∑ i, β i * (s i * t i)) ^ 2 ≤ (∑ i, β i * s i ^ 2) * (∑ i, β i * t i ^ 2) :=
by
simpa using Analysis.weighted_inner_sq_le (Finset.univ : Finset ι) β s t
(fun i _ => hβ i)
lemma weighted_cs_simplex_strict reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Strict weighted Cauchy–Schwarz on the simplex slice. For a nonzero total mass M and positive coordinate weights β, if the coordinates of sum to , the coordinates of sum to , and and are distinct vectors, then the weighted inner product is strictly less than the product of the weighted Euclidean norms .
Formal statement
Proof (Lean source)
lemma weighted_cs_simplex_strict (M : ℝ) (hM : M ≠ 0) (β s t : Fin 3 → ℝ)
(hβ : ∀ i, 0 < β i) (hs : ∑ i, s i = M) (ht : ∑ i, t i = M) (hne : s ≠ t) :
(∑ i, β i * (s i * t i)) <
sqrt (∑ i, β i * s i ^ 2) * sqrt (∑ i, β i * t i ^ 2) := by
let P : ℝ := ∑ i, β i * s i ^ 2
let Q : ℝ := ∑ i, β i * t i ^ 2
let R : ℝ := ∑ i, β i * (s i * t i)
have hP_nonneg : 0 ≤ P := by
simp only [P, Fin.sum_univ_three]
nlinarith [mul_nonneg (hβ 0).le (sq_nonneg (s 0)),
mul_nonneg (hβ 1).le (sq_nonneg (s 1)),
mul_nonneg (hβ 2).le (sq_nonneg (s 2))]
have hle : R ^ 2 ≤ P * Q := by
simpa [P, Q, R] using weighted_cs_sq β s t (fun i => (hβ i).le)
have hlt : R ^ 2 < P * Q := by
refine lt_of_le_of_ne hle ?_
intro heq
have hgap_id :
P * Q - R ^ 2 =
β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 +
β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 +
β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 := by
simp only [P, Q, R, Fin.sum_univ_three]
ring
have hgap_zero : P * Q - R ^ 2 = 0 := by nlinarith
have hsum_zero :
β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 +
β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 +
β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 =
0 := by
nlinarith
have h01_nonneg : 0 ≤ β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 :=
mul_nonneg (mul_nonneg (hβ 0).le (hβ 1).le)
(sq_nonneg (s 0 * t 1 - s 1 * t 0))
have h02_nonneg : 0 ≤ β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 :=
mul_nonneg (mul_nonneg (hβ 0).le (hβ 2).le)
(sq_nonneg (s 0 * t 2 - s 2 * t 0))
have h12_nonneg : 0 ≤ β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 :=
mul_nonneg (mul_nonneg (hβ 1).le (hβ 2).le)
(sq_nonneg (s 1 * t 2 - s 2 * t 1))
have h01_zero : β 0 * β 1 * (s 0 * t 1 - s 1 * t 0) ^ 2 = 0 := by
nlinarith
have h02_zero : β 0 * β 2 * (s 0 * t 2 - s 2 * t 0) ^ 2 = 0 := by
nlinarith
have h12_zero : β 1 * β 2 * (s 1 * t 2 - s 2 * t 1) ^ 2 = 0 := by
nlinarith
have h01 : s 0 * t 1 - s 1 * t 0 = 0 := by
have hpos : 0 < β 0 * β 1 := mul_pos (hβ 0) (hβ 1)
have hsquare : (s 0 * t 1 - s 1 * t 0) ^ 2 = 0 :=
resolve_left (mul_eq_zero.mp h01_zero) (ne_of_gt hpos)
exact sq_eq_zero_iff.mp hsquare
have h02 : s 0 * t 2 - s 2 * t 0 = 0 := by
have hpos : 0 < β 0 * β 2 := mul_pos (hβ 0) (hβ 2)
have hsquare : (s 0 * t 2 - s 2 * t 0) ^ 2 = 0 :=
resolve_left (mul_eq_zero.mp h02_zero) (ne_of_gt hpos)
exact sq_eq_zero_iff.mp hsquare
have h12 : s 1 * t 2 - s 2 * t 1 = 0 := by
have hpos : 0 < β 1 * β 2 := mul_pos (hβ 1) (hβ 2)
have hsquare : (s 1 * t 2 - s 2 * t 1) ^ 2 = 0 :=
resolve_left (mul_eq_zero.mp h12_zero) (ne_of_gt hpos)
exact sq_eq_zero_iff.mp hsquare
have h01eq : s 0 * t 1 = s 1 * t 0 := sub_eq_zero.mp h01
have h02eq : s 0 * t 2 = s 2 * t 0 := sub_eq_zero.mp h02
have h12eq : s 1 * t 2 = s 2 * t 1 := sub_eq_zero.mp h12
have hs3 : s 0 + s 1 + s 2 = M := by
simpa only [Fin.sum_univ_three] using hs
have ht3 : t 0 + t 1 + t 2 = M := by
simpa only [Fin.sum_univ_three] using ht
have hst : s = t := by
by_cases ht0 : t 0 = 0
· by_cases ht1 : t 1 = 0
· by_cases ht2 : t 2 = 0
· exfalso
exact hM (by linarith only [ht3, ht0, ht1, ht2])
· have hs2 : s 2 = t 2 := by
have hscale : M * s 2 = M * t 2 := by
calc
M * s 2 = s 2 * M := by ring
_ = s 2 * (t 0 + t 1 + t 2) := by rw [ht3]
_ = (s 0 + s 1 + s 2) * t 2 := by nlinarith only [h02, h12]
_ = M * t 2 := by rw [hs3]
exact mul_left_cancel₀ hM hscale
have hs0 : s 0 = t 0 := by
have hs0_zero : s 0 = 0 := by
have hmul : s 0 * t 2 = 0 := by rw [h02eq, ht0, mul_zero]
exact (mul_eq_zero.mp hmul).resolve_right ht2
rw [hs0_zero, ht0]
have hs1 : s 1 = t 1 := by
have hs1_zero : s 1 = 0 := by
have hmul : s 1 * t 2 = 0 := by rw [h12eq, ht1, mul_zero]
exact (mul_eq_zero.mp hmul).resolve_right ht2
rw [hs1_zero, ht1]
funext i
fin_cases i <;> assumption
· have hs1 : s 1 = t 1 := by
have hscale : M * s 1 = M * t 1 := by
calc
M * s 1 = s 1 * M := by ring
_ = s 1 * (t 0 + t 1 + t 2) := by rw [ht3]
_ = (s 0 + s 1 + s 2) * t 1 := by nlinarith only [h01, h12]
_ = M * t 1 := by rw [hs3]
exact mul_left_cancel₀ hM hscale
have hs0 : s 0 = t 0 := by
have hs0_zero : s 0 = 0 := by
have hmul : s 0 * t 1 = 0 := by rw [h01eq, ht0, mul_zero]
exact (mul_eq_zero.mp hmul).resolve_right ht1
rw [hs0_zero, ht0]
have hs2 : s 2 = t 2 := by
have hmul : t 1 * t 2 = t 1 * s 2 := by
calc
t 1 * t 2 = s 1 * t 2 := by rw [hs1]
_ = s 2 * t 1 := h12eq
_ = t 1 * s 2 := by ring
exact (mul_left_cancel₀ ht1 hmul).symm
funext i
fin_cases i <;> assumption
· have hs0 : s 0 = t 0 := by
have hscale : M * s 0 = M * t 0 := by
calc
M * s 0 = s 0 * M := by ring
_ = s 0 * (t 0 + t 1 + t 2) := by rw [ht3]
_ = (s 0 + s 1 + s 2) * t 0 := by nlinarith only [h01, h02]
_ = M * t 0 := by rw [hs3]
exact mul_left_cancel₀ hM hscale
have hs1 : s 1 = t 1 := by
have hmul : t 0 * t 1 = t 0 * s 1 := by
calc
t 0 * t 1 = s 0 * t 1 := by rw [hs0]
_ = s 1 * t 0 := h01eq
_ = t 0 * s 1 := by ring
exact (mul_left_cancel₀ ht0 hmul).symm
have hs2 : s 2 = t 2 := by
have hmul : t 0 * t 2 = t 0 * s 2 := by
calc
t 0 * t 2 = s 0 * t 2 := by rw [hs0]
_ = s 2 * t 0 := h02eq
_ = t 0 * s 2 := by ring
exact (mul_left_cancel₀ ht0 hmul).symm
funext i
fin_cases i <;> assumption
exact hne hst
have hsqrt_lt : sqrt (R ^ 2) < sqrt (P * Q) :=
Real.sqrt_lt_sqrt (sq_nonneg R) hlt
have hR_le_sqrt : R ≤ sqrt (R ^ 2) := by
rw [Real.sqrt_sq_eq_abs]
exact le_abs_self R
calc
(∑ i, β i * (s i * t i)) = R := by rfl
_ ≤ sqrt (R ^ 2) := hR_le_sqrt
_ < sqrt (P * Q) := hsqrt_lt
_ = sqrt P * sqrt Q := by rw [Real.sqrt_mul hP_nonneg]
_ = sqrt (∑ i, β i * s i ^ 2) * sqrt (∑ i, β i * t i ^ 2) := by rfl
WeightedSimplexExists 2 core · 4 supporting For κ > 0 there is an admissible support/multiplier pair (S, λ). ★ exists_admissible
Existence of an admissible support (κ > 0)
For κ > 0 there is an admissible support/multiplier pair (S, λ). Constructed by the
intermediate value theorem applied to the continuous threshold function
G(λ) = Σᵢ (max(λ − αᵢ, 0))² / βᵢ: G is continuous with G(min α) = 0 < κ² and
G large for λ large, so some λ has G(λ) = κ²; then S = {i : αᵢ < λ} is
admissible (the truncation makes the sum over S agree with G(λ), and off S,
αⱼ ≥ λ).
def kktThreshold reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The threshold function G(λ) = Σᵢ (max(λ − αᵢ, 0))² / βᵢ whose level set G(λ) = κ² selects the active support.
Definition (Lean source)
noncomputable def kktThreshold (α β : Fin 3 → ℝ) (lam : ℝ) : ℝ :=
∑ i, (max (lam - α i) 0) ^ 2 / β i
lemma exists_admissible reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Existence of an admissible support/multiplier pair (κ > 0). For positive coordinate weights β and a positive SOCP scale κ, there exists a nonempty index set S and a multiplier λ such that , with on S and off S.
Formal statement
hypotheses
conclusion
Proof (Lean source)
lemma exists_admissible (α β : Fin 3 → ℝ) (kappa : ℝ)
(hβ : ∀ i, 0 < β i) (hk : 0 < kappa) :
∃ (S : Finset (Fin 3)) (lam : ℝ), IsAdmissibleSupport α β kappa S lam := by
classical
obtain ⟨kmin, hmin⟩ := (Finite.exists_min α : ∃ k : Fin 3, ∀ i, α k ≤ α i)
obtain ⟨kmax, hmax⟩ := (Finite.exists_max α : ∃ k : Fin 3, ∀ i, α i ≤ α k)
let lo : ℝ := α kmin
let hi : ℝ := α kmax + kappa * sqrt (β kmax)
have hlo_zero : kktThreshold α β lo = 0 := by
exact kktThreshold_eq_zero_of_le α β lo (by intro i; exact hmin i)
have hhi_summand :
(max (hi - α kmax) 0) ^ 2 / β kmax = kappa ^ 2 := by
have hβpos : 0 < β kmax := hβ kmax
have hβnonneg : 0 ≤ β kmax := le_of_lt hβpos
have hsqrt_sq : sqrt (β kmax) ^ 2 = β kmax :=
Real.sq_sqrt hβnonneg
have hdiff : hi - α kmax = kappa * sqrt (β kmax) := by
simp [hi]
have hdiff_nonneg : 0 ≤ hi - α kmax := by
rw [hdiff]
exact mul_nonneg (le_of_lt hk) (Real.sqrt_nonneg _)
rw [max_eq_left hdiff_nonneg, hdiff]
field_simp [ne_of_gt hβpos]
rw [hsqrt_sq]
have hhi_ge : kappa ^ 2 ≤ kktThreshold α β hi := by
calc
kappa ^ 2 = (max (hi - α kmax) 0) ^ 2 / β kmax := by
exact hhi_summand.symm
_ ≤ kktThreshold α β hi := by
unfold kktThreshold
exact Finset.single_le_sum (s := univ)
(f := fun i => (max (hi - α i) 0) ^ 2 / β i)
(fun i _ => div_nonneg (sq_nonneg _) (le_of_lt (hβ i)))
(Finset.mem_univ kmax)
have hlohi : lo ≤ hi := by
have hmul_nonneg : 0 ≤ kappa * sqrt (β kmax) :=
mul_nonneg (le_of_lt hk) (Real.sqrt_nonneg _)
have hle_max : α kmin ≤ α kmax := hmin kmax
dsimp [lo, hi]
linarith
have htarget :
kappa ^ 2 ∈ Icc (kktThreshold α β lo) (kktThreshold α β hi) := by
constructor
· rw [hlo_zero]
exact sq_nonneg kappa
· exact hhi_ge
have hcontOn :
ContinuousOn (kktThreshold α β) (Icc lo hi) :=
(continuous_kktThreshold α β).continuousOn
obtain ⟨lam, -, hlam⟩ :=
intermediate_value_Icc hlohi hcontOn htarget
let S : Finset (Fin 3) := Finset.univ.filter (fun i : Fin 3 => α i < lam)
refine ⟨S, lam, ?_⟩
have hsum_eq : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2 := by
calc
(∑ i ∈ S, (lam - α i) ^ 2 / β i)
= kktThreshold α β lam := by
simpa [S] using support_sum_eq_kktThreshold α β lam
_ = kappa ^ 2 := hlam
refine ⟨?_, hsum_eq, ?_, ?_⟩
· by_contra hnonempty
have hSempty : S = ∅ := by
exact Finset.not_nonempty_iff_eq_empty.mp hnonempty
have hzero : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = 0 := by
simp [hSempty]
have hsquare_zero : kappa ^ 2 = 0 := by
simpa [hzero] using hsum_eq.symm
exact (ne_of_gt (sq_pos_of_pos hk)) hsquare_zero
· intro i hi
simpa [S] using hi
· intro j hj
have hnot : ¬ α j < lam := by
intro hlt
exact hj (by simp [S, hlt])
exact not_lt.mp hnot
4 supporting declarations (lemmas, instances)
-
continuous_kktThresholdlemma — The active-set threshold function varies continuously with the multiplier because the weights are fixed real coefficients.Proof (Lean source)
lemma continuous_kktThreshold (α β : Fin 3 → ℝ) : Continuous (kktThreshold α β) := by unfold kktThreshold continuity -
kktThreshold_nonneglemma — The active-set threshold is nonnegative when every coordinate has a nonnegative weight, because it sums squared multiplier gaps divided by those weights.Proof (Lean source)
lemma kktThreshold_nonneg (α β : Fin 3 → ℝ) (hβ : ∀ i, 0 ≤ β i) (lam : ℝ) : 0 ≤ kktThreshold α β lam := by unfold kktThreshold exact sum_nonneg fun i _ => div_nonneg (sq_nonneg _) (hβ i) -
kktThreshold_eq_zero_of_lelemma — The active-set threshold is zero when the multiplier is no larger than every coefficient.Proof (Lean source)
lemma kktThreshold_eq_zero_of_le (α β : Fin 3 → ℝ) (lam : ℝ) (hle : ∀ i, lam ≤ α i) : kktThreshold α β lam = 0 := by unfold kktThreshold apply Finset.sum_eq_zero intro i _ have hdiff : lam - α i ≤ 0 := by linarith [hle i] simp [max_eq_right hdiff] -
support_sum_eq_kktThresholdlemma — Summing squared multiplier gaps only over coordinates whose coefficients lie below the multiplier gives exactly the active-set threshold.hypothesesα β :Fin 3 → ℝlam :ℝconclusion(∑ i ∈ Finset.univ.filter (fun i : Fin 3 => α i < lam), (lam - α i) ^ 2 / β i)= kktThreshold α β lamProof (Lean source)
lemma support_sum_eq_kktThreshold (α β : Fin 3 → ℝ) (lam : ℝ) : (∑ i ∈ Finset.univ.filter (fun i : Fin 3 => α i < lam), (lam - α i) ^ 2 / β i) = kktThreshold α β lam := by classical calc (∑ i ∈ Finset.univ.filter (fun i : Fin 3 => α i < lam), (lam - α i) ^ 2 / β i) = ∑ i, if α i < lam then (lam - α i) ^ 2 / β i else 0 := by simpa using (Finset.sum_filter (s := univ) (p := fun i : Fin 3 => α i < lam) (f := fun i => (lam - α i) ^ 2 / β i)) _ = kktThreshold α β lam := by unfold kktThreshold apply Finset.sum_congr rfl intro i _ by_cases hi : α i < lam · have hdiff : 0 ≤ lam - α i := by linarith simp [hi, max_eq_left hdiff] · have hdiff : lam - α i ≤ 0 := by linarith [not_lt.mp hi] simp [hi, max_eq_right hdiff]
WeightedSimplexFace 1 core · 1 supporting At κ = 0 the objective wsObj α β 0 is the linear functional Σ αᵢ tᵢ, whose minimizers over Δ_M are exactly the exposed α-minimizing face exposedMinFace. ★ kappa_zero_face
The κ = 0 exposed face
At κ = 0 the objective wsObj α β 0 is the linear functional Σ αᵢ tᵢ, whose
minimizers over Δ_M are exactly the exposed α-minimizing face exposedMinFace.
lemma kappa_zero_face reviewed
⚑ flagged
Causalean.Mathlib.Optimization
The κ = 0 minimizer set is the exposed α-minimizing face. For a simplex budget M, a linear weight vector α, and a candidate point t, t lies in the simplex of budget M and minimizes the linear objective Σᵢ αᵢtᵢ over that simplex if and only if t belongs to the exposed α-minimizing face of the simplex.
Formal statement
hypotheses
conclusion
(InSimplex M t ∧ ∀ s : Fin 3 → ℝ, InSimplex M s → (∑ i, α i * t i) ≤ ∑ i, α i * s i)
↔ t ∈ exposedMinFace M α
Proof (Lean source)
lemma kappa_zero_face (M : ℝ) (α : Fin 3 → ℝ) (t : Fin 3 → ℝ) :
(InSimplex M t ∧
∀ s : Fin 3 → ℝ, InSimplex M s →
(∑ i, α i * t i) ≤ ∑ i, α i * s i)
↔ t ∈ exposedMinFace M α := by
classical
obtain ⟨k, hk⟩ := (Finite.exists_min α : ∃ k, ∀ i, α k ≤ α i)
constructor
· rintro ⟨htS, hmin⟩
refine ⟨htS, ?_⟩
intro i hti j
let v : Fin 3 → ℝ := fun i => if i = k then M else 0
have hM_nonneg : 0 ≤ M := by
rw [← htS.2]
exact sum_nonneg (fun i _ => htS.1 i)
have hv : InSimplex M v := by
constructor
· intro i
dsimp [v]
by_cases hi : i = k
· simp [hi, hM_nonneg]
· simp [hi]
· dsimp [v]
fin_cases k <;> simp [Fin.sum_univ_three]
have hv_sum : ∑ i, α i * v i = α k * M := by
dsimp [v]
fin_cases k <;> simp
have ht_le : ∑ i, α i * t i ≤ α k * M := by
have h := hmin v hv
simpa [hv_sum] using h
have hsum_diff_le : ∑ i, (α i - α k) * t i ≤ 0 := by
have hconst : ∑ i, α k * t i = α k * M := by
rw [← Finset.mul_sum, htS.2]
calc
∑ i, (α i - α k) * t i
= ∑ i, α i * t i - ∑ i, α k * t i := by
simp_rw [sub_mul]
rw [Finset.sum_sub_distrib]
_ = ∑ i, α i * t i - α k * M := by rw [hconst]
_ ≤ 0 := by linarith
have hterm_nonneg (i : Fin 3) : 0 ≤ (α i - α k) * t i := by
exact mul_nonneg (sub_nonneg.mpr (hk i)) (htS.1 i)
have hsum_three :
(α 0 - α k) * t 0 + (α 1 - α k) * t 1 + (α 2 - α k) * t 2 ≤ 0 := by
simpa [Fin.sum_univ_three] using hsum_diff_le
have hterm0 : (α 0 - α k) * t 0 = 0 := by
have h0 := hterm_nonneg 0
have h1 := hterm_nonneg 1
have h2 := hterm_nonneg 2
nlinarith
have hterm1 : (α 1 - α k) * t 1 = 0 := by
have h0 := hterm_nonneg 0
have h1 := hterm_nonneg 1
have h2 := hterm_nonneg 2
nlinarith
have hterm2 : (α 2 - α k) * t 2 = 0 := by
have h0 := hterm_nonneg 0
have h1 := hterm_nonneg 1
have h2 := hterm_nonneg 2
nlinarith
have hterm_zero (i : Fin 3) : (α i - α k) * t i = 0 := by
fin_cases i <;> simp [hterm0, hterm1, hterm2]
have hai : α i = α k := by
exact sub_eq_zero.mp ((mul_eq_zero.mp (hterm_zero i)).resolve_right hti)
rw [hai]
exact hk j
· intro htFace
rcases htFace with ⟨htS, hface⟩
refine ⟨htS, ?_⟩
intro s hsS
have ht_term_eq (i : Fin 3) : α i * t i = α k * t i := by
by_cases hti : t i = 0
· simp [hti]
· have hik : α i ≤ α k := hface i hti k
have hki : α k ≤ α i := hk i
rw [le_antisymm hik hki]
have ht_sum : ∑ i, α i * t i = α k * M := by
calc
∑ i, α i * t i = ∑ i, α k * t i := by
exact Finset.sum_congr rfl (by intro i _; exact ht_term_eq i)
_ = α k * M := by
rw [← Finset.mul_sum, htS.2]
have hs_term_le (i : Fin 3) : α k * s i ≤ α i * s i := by
have hnonneg : 0 ≤ (α i - α k) * s i :=
mul_nonneg (sub_nonneg.mpr (hk i)) (hsS.1 i)
nlinarith
have hs_sum : α k * M ≤ ∑ i, α i * s i := by
calc
α k * M = ∑ i, α k * s i := by
rw [← hsS.2, Finset.mul_sum]
_ ≤ ∑ i, α i * s i := by
exact Finset.sum_le_sum (by intro i _; exact hs_term_le i)
linarith
1 supporting declaration (lemmas, instances)
-
wsObj_kappa_zerolemma — At κ = 0 the weighted-simplex objective collapses to the linear form Σ αᵢ tᵢ.Proof (Lean source)
@[simp] lemma wsObj_kappa_zero (α β : Fin 3 → ℝ) (t : Fin 3 → ℝ) : wsObj α β 0 t = ∑ i, α i * t i := by simp [wsObj]
WeightedSimplexKKT 2 core · 4 supporting Given admissible support/multiplier data (S, λ) for the weighted-simplex SOCP with κ > 0, the induced activeSetPoint lies in Δ_M, has support exactly S, weighted squared norm (Mκ / D)² with D = Σ_{h∈S}(λ−αₕ)/βₕ, objectiv ★ activeSetPoint_value★ activeSetPoint_strict_min
Active-set KKT lemmas (κ > 0)
Given admissible support/multiplier data (S, λ) for the weighted-simplex SOCP with
κ > 0, the induced activeSetPoint lies in Δ_M, has support exactly S, weighted
squared norm (Mκ / D)² with D = Σ_{h∈S}(λ−αₕ)/βₕ, objective value M·λ, and is the
strict minimizer of the SOCP over Δ_M.
lemma activeSetPoint_value reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Objective value of the active-set point. For a nonnegative total mass M, positive weights on the support S, a positive SOCP scale κ, a nonempty support S, strict activity on S, and the admissibility identity , the objective wsObj evaluated at the induced active-set point equals the closed form .
Formal statement
hypotheses
hM :
0 ≤ M
hβ :
∀ i ∈ S, 0 < β i
hk :
0 < kappa
hS :
S.Nonempty
hactive :
∀ i ∈ S, α i < lam
hsq :
(∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2
conclusion
wsObj α β kappa (activeSetPoint M α β S lam) = M * lam
Proof (Lean source)
lemma activeSetPoint_value (hM : 0 ≤ M) (hβ : ∀ i ∈ S, 0 < β i) (hk : 0 < kappa)
(hS : S.Nonempty) (hactive : ∀ i ∈ S, α i < lam)
(hsq : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2) :
wsObj α β kappa (activeSetPoint M α β S lam) = M * lam := by
let D := ∑ h ∈ S, (lam - α h) / β h
have hDpos : 0 < D := activeSet_denom_pos α β S lam hβ hS hactive
have hD : D ≠ 0 := ne_of_gt hDpos
have hnorm :
(∑ i, β i * activeSetPoint M α β S lam i ^ 2) = (M * kappa) ^ 2 / D ^ 2 := by
simpa [D] using activeSetPoint_normSq M α β kappa S lam hβ hS hactive hsq
have hsqrt :
sqrt (∑ i, β i * activeSetPoint M α β S lam i ^ 2) = M * kappa / D := by
rw [hnorm]
rw [div_eq_mul_inv]
rw [show (M * kappa) ^ 2 * (D ^ 2)⁻¹ = (M * kappa / D) ^ 2 by
field_simp [hD]]
exact Real.sqrt_sq (div_nonneg (mul_nonneg hM (le_of_lt hk)) hDpos.le)
have hlin :
(∑ i, α i * activeSetPoint M α β S lam i) = M * lam - M * kappa ^ 2 / D := by
have hcore :
(∑ i ∈ S, α i * ((lam - α i) / β i)) = lam * D - kappa ^ 2 := by
calc
(∑ i ∈ S, α i * ((lam - α i) / β i))
= ∑ i ∈ S,
(lam * ((lam - α i) / β i) - (lam - α i) ^ 2 / β i) := by
apply Finset.sum_congr rfl
intro i hi
have hb : β i ≠ 0 := ne_of_gt (hβ i hi)
field_simp [hb]
ring
_ = lam * D - kappa ^ 2 := by
rw [Finset.sum_sub_distrib, ← Finset.mul_sum]
rw [show (∑ x ∈ S, (lam - α x) / β x) = D by rfl, hsq]
calc
(∑ i, α i * activeSetPoint M α β S lam i)
= ∑ i ∈ S, α i * (M * ((lam - α i) / β i) / D) := by
simp [activeSetPoint, D]
_ = M / D * (∑ i ∈ S, α i * ((lam - α i) / β i)) := by
rw [Finset.mul_sum]
simp [mul_assoc, mul_comm, mul_left_comm, div_eq_mul_inv]
_ = M * lam - M * kappa ^ 2 / D := by
rw [hcore]
field_simp [hD]
calc
wsObj α β kappa (activeSetPoint M α β S lam)
= (∑ i, α i * activeSetPoint M α β S lam i) +
kappa * sqrt (∑ i, β i * activeSetPoint M α β S lam i ^ 2) := rfl
_ = M * lam := by
rw [hlin, hsqrt]
field_simp [hD]
ring
lemma activeSetPoint_strict_min reviewed
⚑ flagged
Causalean.Mathlib.Optimization
Strict minimality of the active-set point (κ > 0). For a positive total mass M, positive coordinate weights β, a positive SOCP scale κ, and a KKT-admissible support/multiplier pair (S, λ), every other point of the simplex has strictly larger objective value than the induced active-set point.
Formal statement
hypotheses
conclusion
∀ s : Fin 3 → ℝ
Proof (Lean source)
lemma activeSetPoint_strict_min (hM : 0 < M) (hβ : ∀ i, 0 < β i) (hk : 0 < kappa)
(hadm : IsAdmissibleSupport α β kappa S lam) :
∀ s : Fin 3 → ℝ, InSimplex M s → s ≠ activeSetPoint M α β S lam →
wsObj α β kappa (activeSetPoint M α β S lam) < wsObj α β kappa s := by
intro s hs hne
let t := activeSetPoint M α β S lam
let D := ∑ h ∈ S, (lam - α h) / β h
let Q := ∑ i, β i * t i ^ 2
let N := sqrt Q
let Ns := sqrt (∑ i, β i * s i ^ 2)
let R := ∑ i, β i * (t i * s i)
have htmem : InSimplex M t := by
simpa [t] using activeSetPoint_mem M α β S lam hM.le (fun i _ => hβ i)
hadm.1 hadm.2.2.1
have ht_sum : ∑ i, t i = M := htmem.2
have hDpos : 0 < D := activeSet_denom_pos α β S lam (fun i _ => hβ i)
hadm.1 hadm.2.2.1
have hD : D ≠ 0 := ne_of_gt hDpos
have hQnorm : Q = (M * kappa) ^ 2 / D ^ 2 := by
simpa [Q, t, D] using activeSetPoint_normSq M α β kappa S lam (fun i _ => hβ i)
hadm.1 hadm.2.2.1 hadm.2.1
have hQnonneg : 0 ≤ Q := by
rw [hQnorm]
exact div_nonneg (sq_nonneg (M * kappa)) (sq_nonneg D)
have hQeq : Q = N ^ 2 := by
rw [Real.sq_sqrt hQnonneg]
have hNval : N = M * kappa / D := by
dsimp [N]
rw [hQnorm]
rw [div_eq_mul_inv]
rw [show (M * kappa) ^ 2 * (D ^ 2)⁻¹ = (M * kappa / D) ^ 2 by
field_simp [hD]]
exact Real.sqrt_sq (le_of_lt (div_pos (mul_pos hM hk) hDpos))
have hNpos : 0 < N := by
rw [hNval]
exact div_pos (mul_pos hM hk) hDpos
have hcs : R < N * Ns := by
simpa [R, N, Ns, t] using
weighted_cs_simplex_strict M hM.ne' β t s hβ ht_sum hs.2 (Ne.symm hne)
have hRdiff :
(∑ i, β i * (t i * (s i - t i))) = R - Q := by
dsimp [R, Q]
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro i hi
ring
have hnorm_strict :
(kappa / N) * (∑ i, β i * (t i * (s i - t i))) <
kappa * (Ns - N) := by
rw [hRdiff, hQeq]
field_simp [ne_of_gt hNpos]
nlinarith [mul_pos hk hNpos]
have hstationary :
(kappa / N) * (∑ i, β i * (t i * (s i - t i))) =
∑ i ∈ S, (lam - α i) * (s i - t i) := by
subst t
calc
(kappa / N) *
(∑ i,
β i * (activeSetPoint M α β S lam i * (s i - activeSetPoint M α β S lam i)))
= ∑ i ∈ S,
(kappa / N) *
(β i * (M * ((lam - α i) / β i) / D *
(s i - activeSetPoint M α β S lam i))) := by
rw [Finset.mul_sum]
simp [activeSetPoint, D]
_ = ∑ i ∈ S, (lam - α i) * (s i - activeSetPoint M α β S lam i) := by
apply Finset.sum_congr rfl
intro i hi
simp [activeSetPoint, hi, D]
rw [hNval]
rw [show (∑ h ∈ S, (lam - α h) / β h) = D by rfl]
field_simp [ne_of_gt hM, ne_of_gt hk, hD, ne_of_gt (hβ i)]
have hgap_formula :
wsObj α β kappa s - wsObj α β kappa t =
(∑ i, α i * (s i - t i)) + kappa * (Ns - N) := by
subst t
dsimp [wsObj, Ns, N, Q]
have hsumdiff :
(∑ i, α i * (s i - activeSetPoint M α β S lam i)) =
(∑ i, α i * s i) - ∑ i, α i * activeSetPoint M α β S lam i := by
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro i hi
ring
rw [hsumdiff]
ring
have hremainder_eq :
(∑ i, α i * (s i - t i)) +
(∑ i ∈ S, (lam - α i) * (s i - t i))
= (∑ i, (if i ∈ S then lam else α i) * s i) - lam * M := by
subst t
have hcoeff :
(∑ i, α i * (s i - activeSetPoint M α β S lam i)) +
(∑ i ∈ S, (lam - α i) * (s i - activeSetPoint M α β S lam i))
= ∑ i, (if i ∈ S then lam else α i) *
(s i - activeSetPoint M α β S lam i) := by
rw [show (∑ i ∈ S, (lam - α i) * (s i - activeSetPoint M α β S lam i)) =
∑ i, if i ∈ S then
(lam - α i) * (s i - activeSetPoint M α β S lam i) else 0 by
simp]
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro i hi
by_cases his : i ∈ S
· simp [his]
ring
· simp [his]
have hmass :
(∑ i, (if i ∈ S then lam else α i) * activeSetPoint M α β S lam i) =
lam * M := by
calc
(∑ i, (if i ∈ S then lam else α i) * activeSetPoint M α β S lam i)
= ∑ i, lam * activeSetPoint M α β S lam i := by
apply Finset.sum_congr rfl
intro i hi
by_cases his : i ∈ S
· simp [his]
· simp [activeSetPoint, his]
_ = lam * M := by
rw [← Finset.mul_sum, ht_sum]
rw [hcoeff]
rw [show (∑ i, (if i ∈ S then lam else α i) *
(s i - activeSetPoint M α β S lam i)) =
(∑ i, (if i ∈ S then lam else α i) * s i) -
∑ i, (if i ∈ S then lam else α i) * activeSetPoint M α β S lam i by
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro i hi
ring]
rw [hmass]
have hremainder_nonneg :
0 ≤ (∑ i, α i * (s i - t i)) +
(∑ i ∈ S, (lam - α i) * (s i - t i)) := by
rw [hremainder_eq]
have hpoint : ∀ i, lam * s i ≤ (if i ∈ S then lam else α i) * s i := by
intro i
by_cases hi : i ∈ S
· simp [hi]
· exact mul_le_mul_of_nonneg_right (by simpa [hi] using hadm.2.2.2 i hi) (hs.1 i)
have hsum :
(∑ i, lam * s i) ≤ ∑ i, (if i ∈ S then lam else α i) * s i := by
exact Finset.sum_le_sum (fun i hi => hpoint i)
rw [← Finset.mul_sum, hs.2] at hsum
linarith
have hgap_pos : 0 < wsObj α β kappa s - wsObj α β kappa t := by
have hstrict :
(∑ i, α i * (s i - t i)) + (∑ i ∈ S, (lam - α i) * (s i - t i)) <
wsObj α β kappa s - wsObj α β kappa t := by
rw [hgap_formula]
rw [hstationary] at hnorm_strict
linarith
linarith
have ht_value : wsObj α β kappa t = M * lam := by
simpa [t] using activeSetPoint_value M α β kappa S lam hM.le (fun i _ => hβ i) hk
hadm.1 hadm.2.2.1 hadm.2.1
linarith
4 supporting declarations (lemmas, instances)
-
activeSet_denom_poslemma — The active-set denominator D = Σ_{h∈S} (λ−αₕ)/βₕ is strictly positive: S is nonempty and each summand is positive (λ > αₕ on S, βₕ > 0).hypotheseshβ :∀ i ∈ S, 0 < β ihS :S.Nonemptyhactive :∀ i ∈ S, α i < lamconclusion0 < ∑ h ∈ S, (lam - α h) / β hProof (Lean source)
lemma activeSet_denom_pos (hβ : ∀ i ∈ S, 0 < β i) (hS : S.Nonempty) (hactive : ∀ i ∈ S, α i < lam) : 0 < ∑ h ∈ S, (lam - α h) / β h := by exact Finset.sum_pos (fun h hh => div_pos (sub_pos.mpr (hactive h hh)) (hβ h hh)) hS -
activeSetPoint_pos_ifflemma — The active-set point has support exactly S: on S its coordinate is positive, off S it is 0.hypothesesconclusion0 < activeSetPoint M α β S lam i ↔ i ∈ SProof (Lean source)
lemma activeSetPoint_pos_iff (hM : 0 < M) (hβ : ∀ i ∈ S, 0 < β i) (hS : S.Nonempty) (hactive : ∀ i ∈ S, α i < lam) (i : Fin 3) : 0 < activeSetPoint M α β S lam i ↔ i ∈ S := by constructor · intro hpos by_contra hi simp [activeSetPoint, hi] at hpos · intro hi rw [activeSetPoint, if_pos hi] exact div_pos (mul_pos hM (div_pos (sub_pos.mpr (hactive i hi)) (hβ i hi))) (activeSet_denom_pos α β S lam hβ hS hactive) -
activeSetPoint_memlemma — The active-set point lies in the simplex Δ_M.hypotheseshM :0 ≤ Mhβ :∀ i ∈ S, 0 < β ihS :S.Nonemptyhactive :∀ i ∈ S, α i < lamconclusionInSimplex M (activeSetPoint M α β S lam)Proof (Lean source)
lemma activeSetPoint_mem (hM : 0 ≤ M) (hβ : ∀ i ∈ S, 0 < β i) (hS : S.Nonempty) (hactive : ∀ i ∈ S, α i < lam) : InSimplex M (activeSetPoint M α β S lam) := by constructor · intro i by_cases hi : i ∈ S · rw [activeSetPoint, if_pos hi] exact div_nonneg (mul_nonneg hM (le_of_lt (div_pos (sub_pos.mpr (hactive i hi)) (hβ i hi)))) (le_of_lt (activeSet_denom_pos α β S lam hβ hS hactive)) · simp [activeSetPoint, hi] · let D := ∑ h ∈ S, (lam - α h) / β h have hD : D ≠ 0 := ne_of_gt (activeSet_denom_pos α β S lam hβ hS hactive) calc (∑ i, activeSetPoint M α β S lam i) = ∑ i ∈ S, M * ((lam - α i) / β i) / D := by simp [activeSetPoint, D] _ = M / D * (∑ i ∈ S, (lam - α i) / β i) := by rw [Finset.mul_sum] simp [D, mul_assoc, mul_comm, mul_left_comm, div_eq_mul_inv] _ = M := by rw [show (∑ i ∈ S, (lam - α i) / β i) = D by rfl] field_simp [hD] -
activeSetPoint_normSqlemma — Weighted squared norm of the active-set point: Σ βᵢ tᵢ² = (Mκ)² / D², using the admissibility identity Σ_{i∈S}(λ−αᵢ)²/βᵢ = κ².hypotheseshβ :∀ i ∈ S, 0 < β ihS :S.Nonemptyhactive :∀ i ∈ S, α i < lamhsq :(∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2conclusion(∑ i, β i * activeSetPoint M α β S lam i ^ 2)= (M * kappa) ^ 2 / (∑ h ∈ S, (lam - α h) / β h) ^ 2Proof (Lean source)
lemma activeSetPoint_normSq (hβ : ∀ i ∈ S, 0 < β i) (hS : S.Nonempty) (hactive : ∀ i ∈ S, α i < lam) (hsq : (∑ i ∈ S, (lam - α i) ^ 2 / β i) = kappa ^ 2) : (∑ i, β i * activeSetPoint M α β S lam i ^ 2) = (M * kappa) ^ 2 / (∑ h ∈ S, (lam - α h) / β h) ^ 2 := by let D := ∑ h ∈ S, (lam - α h) / β h have hD : D ≠ 0 := ne_of_gt (activeSet_denom_pos α β S lam hβ hS hactive) calc (∑ i, β i * activeSetPoint M α β S lam i ^ 2) = ∑ i ∈ S, β i * (M * ((lam - α i) / β i) / D) ^ 2 := by simp [activeSetPoint, D] _ = ∑ i ∈ S, (M ^ 2 / D ^ 2) * ((lam - α i) ^ 2 / β i) := by apply Finset.sum_congr rfl intro i hi have hb : β i ≠ 0 := ne_of_gt (hβ i hi) field_simp [hb, hD] _ = (M ^ 2 / D ^ 2) * (∑ i ∈ S, (lam - α i) ^ 2 / β i) := by rw [Finset.mul_sum] _ = (M * kappa) ^ 2 / D ^ 2 := by rw [hsq] ring