Mathlib.Optimization.Affine.SignCell
Optimization over regions determined by affine sign restrictions, including closure, common-slack, extrema, and polynomial formulations.
Basic 10 core · 7 supporting This module defines finite systems of real affine inequalities with individually weak or strict comparisons, together with their strict cells and weak relaxations. ★ isClosed_weakCell
Finite affine sign cells
This module defines finite systems of real affine inequalities with individually weak or strict comparisons, together with their strict cells and weak relaxations. It proves that the weak relaxation is a closed convex set.
structure AffineFn reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite number of coordinates, an affine real-valued function is specified by one coefficient for each coordinate and one constant term.
Definition (Lean source)
parameters
n :
ℕ
fields
def eval reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell.AffineFn
Given an affine function and a coordinate vector, its evaluated real value is given by the finite coefficient-weighted sum plus the constant.
inductive ConstraintKind reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
A constraint kind records whether its affine inequality is weak or strict.
Definition (Lean source)
inductive
ConstraintKind :
Type
constructors
weak :
The constraint is interpreted with a weak comparison.
strict :
The constraint is interpreted with a strict comparison.
deriving DecidableEq
structure Constraint reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite number of coordinates, a marked affine constraint contains its normalized affine left-hand side and its weak-or-strict mark.
Definition (Lean source)
parameters
n :
ℕ
fields
The affine left-hand side, normalized against zero.
fn :
AffineFn n
Whether the normalized inequality is weak or strict.
kind :
abbrev AffineSystem reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite number of coordinates, an affine constraint system is given by a finite list of marked affine constraints.
Definition (Lean source)
def strictHolds reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell.Constraint
Given a marked affine constraint and a coordinate vector, the original constraint-satisfaction condition uses the comparison selected by the constraint's mark.
Definition (Lean source)
parameters
def
strictHolds c x :
Prop
given by
match c.kind with | .weak => c.fn.eval x ≤ 0 | .strict => c.fn.eval x < 0
def weakHolds reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell.Constraint
Given a marked affine constraint and a coordinate vector, the weak constraint-satisfaction condition is given by the nonpositive affine evaluation.
Definition (Lean source)
def strictCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, its strict cell is given by the points satisfying every listed constraint using its original comparison.
Definition (Lean source)
parameters
n :
ℕ
Γ :
given by
{x | ∀ c ∈ Γ, c.strictHolds x}
def weakCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, its weak relaxation is given by the points weakly satisfying every listed constraint.
Definition (Lean source)
parameters
n :
ℕ
Γ :
given by
{x | ∀ c ∈ Γ, c.weakHolds x}
theorem isClosed_weakCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, its weak relaxation is closed.
Formal statement
Proof (Lean source)
theorem isClosed_weakCell {n : ℕ} (Γ : AffineSystem n) : IsClosed (weakCell Γ) := by
induction Γ with
| nil => simp [weakCell]
| cons c Γ ih =>
rw [show weakCell (c :: Γ) = {x | c.fn.eval x ≤ 0} ∩ weakCell Γ by
ext x
simp [weakCell, Constraint.weakHolds]]
exact (isClosed_le c.fn.continuous_eval continuous_const).inter ih
7 supporting declarations (lemmas, instances)
-
eval_affineCombinationtheorem — Given an affine function, two coordinate vectors, and a real weight, evaluation at their affine combination equals the same affine combination of their evaluations.hypothesesconclusionf.eval ((1 - t) • x + t • y) = (1 - t) * f.eval x + t * f.eval yProof (Lean source)
theorem eval_affineCombination {n : ℕ} (f : AffineFn n) (x y : Fin n → ℝ) (t : ℝ) : f.eval ((1 - t) • x + t • y) = (1 - t) * f.eval x + t * f.eval y := by simp only [eval, Pi.add_apply, Pi.smul_apply, smul_eq_mul] calc (∑ i, f.coeff i * ((1 - t) * x i + t * y i)) + f.constant = (1 - t) * (∑ i, f.coeff i * x i) + t * (∑ i, f.coeff i * y i) + f.constant := by rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib] apply congrArg (fun z => z + f.constant) apply Finset.sum_congr rfl intro i hi ring _ = (1 - t) * ((∑ i, f.coeff i * x i) + f.constant) + t * ((∑ i, f.coeff i * y i) + f.constant) := by ring -
continuous_evaltheorem — Given an affine function, its evaluation map is continuous.Proof (Lean source)
-
instDecidableEqConstraintKindinstancederiving DecidableEq -
mem_strictCelltheorem — Given a point, membership in the strict cell is equivalent to satisfying every listed constraint with its original comparison.Proof (Lean source)
@[simp] theorem mem_strictCell {n : ℕ} {Γ : AffineSystem n} {x : Fin n → ℝ} : x ∈ strictCell Γ ↔ ∀ c ∈ Γ, c.strictHolds x := Iff.rfl -
mem_weakCelltheorem — Given a point, membership in the weak relaxation is equivalent to weakly satisfying every listed constraint.Proof (Lean source)
@[simp] theorem mem_weakCell {n : ℕ} {Γ : AffineSystem n} {x : Fin n → ℝ} : x ∈ weakCell Γ ↔ ∀ c ∈ Γ, c.weakHolds x := Iff.rfl -
strictCell_subset_weakCelltheorem — Given an affine constraint system, every strictly feasible point belongs to its weak relaxation.Proof (Lean source)
theorem strictCell_subset_weakCell {n : ℕ} (Γ : AffineSystem n) : strictCell Γ ⊆ weakCell Γ := by intro x hx c hc have h := hx c hc cases hkind : c.kind with | weak => simpa [Constraint.strictHolds, Constraint.weakHolds, hkind] using h | strict => exact le_of_lt (by simpa [Constraint.strictHolds, hkind] using h) -
convex_weakCelltheorem — Given an affine constraint system, its weak relaxation is convex.Proof (Lean source)
theorem convex_weakCell {n : ℕ} (Γ : AffineSystem n) : Convex ℝ (weakCell Γ) := by intro x hx y hy a b ha hb hab c hc have hxc := hx c hc have hyc := hy c hc unfold Constraint.weakHolds at hxc hyc ⊢ have hab' : a = 1 - b := by linarith rw [hab', AffineFn.eval_affineCombination] exact add_nonpos (mul_nonpos_of_nonneg_of_nonpos (by linarith) hxc) (mul_nonpos_of_nonneg_of_nonpos hb hyc)
Closure 2 core · 4 supporting Given one point satisfying every strict comparison, this module approximates every weakly feasible point by strictly feasible segment points and identifies the weak relaxation as the closure of the strict cell. ★ closure_strictCell_eq_weakCell
Segment approximation and closure of affine sign cells
Given one point satisfying every strict comparison, this module approximates every weakly feasible point by strictly feasible segment points and identifies the weak relaxation as the closure of the strict cell.
def segmentPoint reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a weak endpoint, a distinguished strict endpoint, and a real weight, the segment point is given by placing weight ε on the strict endpoint.
theorem closure_strictCell_eq_weakCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a nonempty strict cell, the closure of that strict cell equals its weak relaxation.
Formal statement
Proof (Lean source)
theorem closure_strictCell_eq_weakCell {n : ℕ} {Γ : AffineSystem n}
(hΓ : (strictCell Γ).Nonempty) : closure (strictCell Γ) = weakCell Γ := by
apply Set.Subset.antisymm
· exact closure_minimal (strictCell_subset_weakCell Γ) (isClosed_weakCell Γ)
· exact weakCell_subset_closure_strictCell hΓ
4 supporting declarations (lemmas, instances)
-
tendsto_segmentPoint_zerotheorem — Given a weak endpoint and a distinguished strict endpoint, their segment points converge to the weak endpoint as the strict-endpoint weight tends to zero.Proof (Lean source)
theorem tendsto_segmentPoint_zero {n : ℕ} (x x₀ : Fin n → ℝ) : Tendsto (segmentPoint x x₀) (𝓝 0) (𝓝 x) := by have h : Continuous (segmentPoint x x₀) := by unfold segmentPoint fun_prop have h0 : Tendsto (segmentPoint x x₀) (𝓝 0) (𝓝 (segmentPoint x x₀ 0)) := h.continuousAt simpa [segmentPoint] using h0 -
segmentPoint_mem_strictCelltheorem — Given a weakly feasible point, a strictly feasible point, a positive segment weight, and a weight at most one, the corresponding segment point is strictly feasible.hypothesesconclusionsegmentPoint x x₀ ε ∈ strictCell ΓProof (Lean source)
theorem segmentPoint_mem_strictCell {n : ℕ} {Γ : AffineSystem n} {x x₀ : Fin n → ℝ} (hx : x ∈ weakCell Γ) (hx₀ : x₀ ∈ strictCell Γ) {ε : ℝ} (hεpos : 0 < ε) (hεone : ε ≤ 1) : segmentPoint x x₀ ε ∈ strictCell Γ := by intro c hc have hxc := hx c hc have hx₀c := hx₀ c hc unfold Constraint.weakHolds at hxc unfold segmentPoint cases hkind : c.kind with | weak => simp only [Constraint.strictHolds, hkind] at hx₀c ⊢ rw [AffineFn.eval_affineCombination] exact add_nonpos (mul_nonpos_of_nonneg_of_nonpos (sub_nonneg.mpr hεone) hxc) (mul_nonpos_of_nonneg_of_nonpos (le_of_lt hεpos) hx₀c) | strict => simp only [Constraint.strictHolds, hkind] at hx₀c ⊢ rw [AffineFn.eval_affineCombination] exact add_neg_of_nonpos_of_neg (mul_nonpos_of_nonneg_of_nonpos (sub_nonneg.mpr hεone) hxc) (mul_neg_of_pos_of_neg hεpos hx₀c) -
exists_strictCell_sequence_tendstotheorem — Given a weakly feasible point and a strictly feasible point, there is a sequence of strictly feasible points converging to the weakly feasible point.hypothesesconclusion∃ u : ℕ → (Fin n → ℝ),Proof (Lean source)
theorem exists_strictCell_sequence_tendsto {n : ℕ} {Γ : AffineSystem n} {x x₀ : Fin n → ℝ} (hx : x ∈ weakCell Γ) (hx₀ : x₀ ∈ strictCell Γ) : ∃ u : ℕ → (Fin n → ℝ), (∀ k, u k ∈ strictCell Γ) ∧ Tendsto u atTop (𝓝 x) := by refine ⟨fun k => segmentPoint x x₀ (1 / ((k : ℝ) + 1)), ?_, ?_⟩ · intro k apply segmentPoint_mem_strictCell hx hx₀ · positivity · apply (div_le_one (by positivity)).2 norm_num · exact (tendsto_segmentPoint_zero x x₀).comp tendsto_one_div_add_atTop_nhds_zero_nat -
weakCell_subset_closure_strictCelltheorem — Given a nonempty strict cell, every point of the weak relaxation belongs to the closure of the strict cell.Proof (Lean source)
theorem weakCell_subset_closure_strictCell {n : ℕ} {Γ : AffineSystem n} (hΓ : (strictCell Γ).Nonempty) : weakCell Γ ⊆ closure (strictCell Γ) := by intro x hx rcases hΓ with ⟨x₀, hx₀⟩ rw [mem_closure_iff_seq_limit] exact exists_strictCell_sequence_tendsto hx hx₀
CommonSlack 4 core · 6 supporting This module gives the bounded Phase-I common-slack characterization of strict feasibility: one positive margin is shared by all strict affine inequalities, while weak inequalities stay weak. ★ strictFeasible_iff_commonSlackValue_pos
Common-slack strict feasibility
This module gives the bounded Phase-I common-slack characterization of strict feasibility: one positive margin is shared by all strict affine inequalities, while weak inequalities stay weak.
def commonSlackFeasible reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, a coordinate vector, and a real slack, the common-slack feasibility condition is given by the slack being nonnegative, the slack being at most one, and every weak constraint evaluating to at most zero while every strict constraint evaluates to at most the negative slack.
Definition (Lean source)
parameters
def
commonSlackFeasible Γ x δ :
Prop
given by
clause 1
0 ≤ δ
clause 2
δ ≤ 1
clause 3
c ∈ Γ :
c.fn.eval x ≤ match c.kind with | .weak => 0 | .strict => -δ
def commonSlackSet reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, its feasible slack set is given by the slacks for which some coordinate vector is common-slack feasible.
Definition (Lean source)
def commonSlackValue reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, its common-slack value is given by the supremum of its feasible slack set.
Definition (Lean source)
theorem strictFeasible_iff_commonSlackValue_pos reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given an affine constraint system, its strict cell is nonempty exactly when its bounded common-slack value is positive.
Formal statement
Proof (Lean source)
theorem strictFeasible_iff_commonSlackValue_pos {n : ℕ} (Γ : AffineSystem n) :
(strictCell Γ).Nonempty ↔ 0 < commonSlackValue Γ := by
constructor
· rintro ⟨x, hx⟩
rcases positiveSlackWitness_of_strictPoint hx with ⟨δ, hδ, hfeas⟩
exact commonSlackValue_pos_of_witness hδ hfeas
· intro hval
rcases positiveSlackWitness_of_commonSlackValue_pos hval with ⟨δ, hδ, x, hx⟩
exact ⟨x, strictPoint_of_positiveSlack hδ hx⟩
6 supporting declarations (lemmas, instances)
-
bddAbove_commonSlackSettheorem — Given an affine constraint system, its feasible slack set is bounded above.Proof (Lean source)
theorem bddAbove_commonSlackSet {n : ℕ} (Γ : AffineSystem n) : BddAbove (commonSlackSet Γ) := by refine ⟨1, ?_⟩ intro δ hδ rcases hδ with ⟨x, hx⟩ exact hx.2.1 -
positiveSlackWitness_of_strictPointtheorem — Given a strictly feasible point, there is a positive common slack for that same point.hypothesesn :hx :x ∈ strictCell ΓProof (Lean source)
theorem positiveSlackWitness_of_strictPoint {n : ℕ} {Γ : AffineSystem n} {x : Fin n → ℝ} (hx : x ∈ strictCell Γ) : ∃ δ : ℝ, 0 < δ ∧ commonSlackFeasible Γ x δ := by induction Γ with | nil => refine ⟨1, by norm_num, ?_⟩ simp [commonSlackFeasible] | cons c Γ ih => have hc : c.strictHolds x := hx c (by simp) have hΓ : x ∈ strictCell Γ := by intro d hd exact hx d (by simp [hd]) rcases ih hΓ with ⟨δ, hδ, hfeas⟩ rcases hfeas with ⟨hδ0, hδ1, htail⟩ cases hk : c.kind with | weak => refine ⟨δ, hδ, hδ0, hδ1, ?_⟩ intro d hd rcases List.mem_cons.mp hd with rfl | hd · simpa [Constraint.strictHolds, hk] using hc · exact htail d hd | strict => let ε := min δ (-c.fn.eval x) have hneg : 0 < -c.fn.eval x := by have hc' : c.fn.eval x < 0 := by simpa [Constraint.strictHolds, hk] using hc exact neg_pos.mpr hc' have hε : 0 < ε := lt_min hδ hneg have hε_head : ε ≤ -c.fn.eval x := min_le_right _ _ refine ⟨ε, hε, le_of_lt hε, (min_le_left _ _).trans hδ1, ?_⟩ intro d hd rcases List.mem_cons.mp hd with rfl | hd · simp only [hk] linarith · have hd' := htail d hd cases hdk : d.kind with | weak => simpa [hdk] using hd' | strict => have hε_le : ε ≤ δ := min_le_left _ _ simp only [hdk] at hd' ⊢ linarith -
strictPoint_of_positiveSlacktheorem — Given a positive slack and a common-slack feasible point, that point belongs to the strict cell.hypothesesconclusionx ∈ strictCell ΓProof (Lean source)
theorem strictPoint_of_positiveSlack {n : ℕ} {Γ : AffineSystem n} {x : Fin n → ℝ} {δ : ℝ} (hδ : 0 < δ) (hx : commonSlackFeasible Γ x δ) : x ∈ strictCell Γ := by intro c hc have hcx := hx.2.2 c hc cases hk : c.kind with | weak => simpa [Constraint.strictHolds, hk] using hcx | strict => simp only [hk] at hcx simp only [Constraint.strictHolds, hk] linarith -
commonSlackValue_pos_of_witnesstheorem — Given a positive slack and a common-slack feasible point, the common-slack value is positive.hypothesesconclusion0 < commonSlackValue ΓProof (Lean source)
theorem commonSlackValue_pos_of_witness {n : ℕ} {Γ : AffineSystem n} {x : Fin n → ℝ} {δ : ℝ} (hδ : 0 < δ) (hx : commonSlackFeasible Γ x δ) : 0 < commonSlackValue Γ := by have hmem : δ ∈ commonSlackSet Γ := ⟨x, hx⟩ have hle : δ ≤ commonSlackValue Γ := by unfold commonSlackValue exact le_csSup (bddAbove_commonSlackSet Γ) hmem exact hδ.trans_le hle -
positiveSlackWitness_of_commonSlackValue_postheorem — Given a positive common-slack value, some feasible slack is positive.hypothesesn :ℕhval :0 < commonSlackValue ΓProof (Lean source)
theorem positiveSlackWitness_of_commonSlackValue_pos {n : ℕ} {Γ : AffineSystem n} (hval : 0 < commonSlackValue Γ) : ∃ δ : ℝ, 0 < δ ∧ δ ∈ commonSlackSet Γ := by have hne : (commonSlackSet Γ).Nonempty := by by_contra h have hempty : commonSlackSet Γ = ∅ := Set.not_nonempty_iff_eq_empty.mp h rw [commonSlackValue, hempty, Real.sSup_empty] at hval exact (lt_irrefl 0 hval) have hhalf : commonSlackValue Γ / 2 < commonSlackValue Γ := by linarith rw [commonSlackValue] at hhalf rcases (lt_csSup_iff (bddAbove_commonSlackSet Γ) hne).mp hhalf with ⟨δ, hδmem, hhalfδ⟩ refine ⟨δ, ?_, hδmem⟩ have hhalf_pos : 0 < commonSlackValue Γ / 2 := by linarith exact hhalf_pos.trans hhalfδ -
commonSlackValue_niltheorem — Given a number of coordinates, the empty system's common-slack value equals one.Proof (Lean source)
theorem commonSlackValue_nil (n : ℕ) : commonSlackValue ([] : AffineSystem n) = 1 := by have hmem : (1 : ℝ) ∈ commonSlackSet ([] : AffineSystem n) := by refine ⟨fun _ => 0, ?_⟩ simp [commonSlackFeasible] apply le_antisymm · unfold commonSlackValue exact csSup_le ⟨1, hmem⟩ fun δ hδ => hδ.choose_spec.2.1 · unfold commonSlackValue exact le_csSup (bddAbove_commonSlackSet ([] : AffineSystem n)) hmem
Example 2 core · 3 supporting This module instantiates the API with the interval cut out by the strict inequality 0 < x and the weak inequality x ≤ 1. ★ closure_strictCell_mixedExample
Mixed strict/weak sign-cell example
This module instantiates the API with the interval cut out by the strict inequality 0 < x
and the weak inequality x ≤ 1.
def mixedExample reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
The mixed one-dimensional example system is given by the strict lower inequality -x < 0 and the weak upper inequality x - 1 ≤ 0.
Definition (Lean source)
def
given by
[ { fn := { coeff := fun _ => -1, constant := 0 }, kind := .strict }, { fn := { coeff := fun _ => 1, constant := -1 }, kind := .weak } ]
theorem closure_strictCell_mixedExample reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
The closure of the example's half-open strict interval equals its closed weak interval.
Formal statement
conclusion
Proof (Lean source)
theorem closure_strictCell_mixedExample :
closure (strictCell mixedExample) = weakCell mixedExample := by
apply closure_strictCell_eq_weakCell
exact ⟨_, half_mem_strictCell_mixedExample⟩
3 supporting declarations (lemmas, instances)
-
mem_strictCell_mixedExampletheorem — Given a one-dimensional coordinate vector, it belongs to the example's strict cell exactly when its coordinate lies above zero and at most one.Proof (Lean source)
theorem mem_strictCell_mixedExample (x : Fin 1 → ℝ) : x ∈ strictCell mixedExample ↔ 0 < x 0 ∧ x 0 ≤ 1 := by simp [strictCell, mixedExample, Constraint.strictHolds, AffineFn.eval] -
mem_weakCell_mixedExampletheorem — Given a one-dimensional coordinate vector, it belongs to the example's weak cell exactly when its coordinate lies between zero and one inclusively.Proof (Lean source)
theorem mem_weakCell_mixedExample (x : Fin 1 → ℝ) : x ∈ weakCell mixedExample ↔ 0 ≤ x 0 ∧ x 0 ≤ 1 := by simp [weakCell, mixedExample, Constraint.weakHolds, AffineFn.eval] -
half_mem_strictCell_mixedExampletheorem — The constant one-half coordinate vector belongs to the example's strict cell.conclusionProof (Lean source)
theorem half_mem_strictCell_mixedExample : (fun _ : Fin 1 => (1 / 2 : ℝ)) ∈ strictCell mixedExample := by rw [mem_strictCell_mixedExample] norm_num
Extrema 1 core · 6 supporting Continuous real objectives have the same bounded infima and suprema on a nonempty strict affine cell and on its weak relaxation. ★ sInf_image_strictCell_eq_weakCell
Preservation of bounded extrema
Continuous real objectives have the same bounded infima and suprema on a nonempty strict affine cell and on its weak relaxation.
theorem sInf_image_strictCell_eq_weakCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a nonempty strict cell, a continuous real objective, and a lower bound for its strict-cell image, the strict and weak image sets have the same infimum.
Formal statement
Proof (Lean source)
theorem sInf_image_strictCell_eq_weakCell {n : ℕ}
{Γ : AffineSystem n} {φ : (Fin n → ℝ) → ℝ}
(hΓ : (strictCell Γ).Nonempty) (hφ : Continuous φ)
(hBdd : BddBelow (φ '' strictCell Γ)) :
sInf (φ '' strictCell Γ) = sInf (φ '' weakCell Γ) := by
have hcl := closure_image_strictCell_eq_closure_image_weakCell hΓ hφ
have hlb : lowerBounds (φ '' strictCell Γ) = lowerBounds (φ '' weakCell Γ) := by
rw [← lowerBounds_closure (φ '' strictCell Γ), hcl, lowerBounds_closure]
have hBdd' := bddBelow_image_weakCell_of_strictCell hΓ hφ hBdd
have hne : (φ '' strictCell Γ).Nonempty := hΓ.image φ
have hne' : (φ '' weakCell Γ).Nonempty := hne.mono (image_mono (strictCell_subset_weakCell Γ))
rw [← csSup_lowerBounds_eq_csInf hBdd hne,
← csSup_lowerBounds_eq_csInf hBdd' hne', hlb]
6 supporting declarations (lemmas, instances)
-
closure_image_strictCell_eq_closure_image_weakCelltheorem — Given a nonempty strict cell and a continuous real objective, the closures of its strict-cell and weak-cell image sets are equal.hypothesesconclusionProof (Lean source)
theorem closure_image_strictCell_eq_closure_image_weakCell {n : ℕ} {Γ : AffineSystem n} {φ : (Fin n → ℝ) → ℝ} (hΓ : (strictCell Γ).Nonempty) (hφ : Continuous φ) : closure (φ '' strictCell Γ) = closure (φ '' weakCell Γ) := by rw [← closure_strictCell_eq_weakCell hΓ, closure_image_closure hφ] -
bddBelow_image_weakCell_of_strictCelltheorem — Given a nonempty strict cell, a continuous real objective, and a lower bound for its strict-cell image, the weak-cell image is bounded below.hypothesesProof (Lean source)
theorem bddBelow_image_weakCell_of_strictCell {n : ℕ} {Γ : AffineSystem n} {φ : (Fin n → ℝ) → ℝ} (hΓ : (strictCell Γ).Nonempty) (hφ : Continuous φ) (hBdd : BddBelow (φ '' strictCell Γ)) : BddBelow (φ '' weakCell Γ) := by have hcl := closure_image_strictCell_eq_closure_image_weakCell hΓ hφ rw [BddBelow, ← lowerBounds_closure (φ '' weakCell Γ), ← hcl, lowerBounds_closure] exact hBdd -
bddAbove_image_weakCell_of_strictCelltheorem — Given a nonempty strict cell, a continuous real objective, and an upper bound for its strict-cell image, the weak-cell image is bounded above.hypothesesProof (Lean source)
theorem bddAbove_image_weakCell_of_strictCell {n : ℕ} {Γ : AffineSystem n} {φ : (Fin n → ℝ) → ℝ} (hΓ : (strictCell Γ).Nonempty) (hφ : Continuous φ) (hBdd : BddAbove (φ '' strictCell Γ)) : BddAbove (φ '' weakCell Γ) := by have hcl := closure_image_strictCell_eq_closure_image_weakCell hΓ hφ rw [BddAbove, ← upperBounds_closure (φ '' weakCell Γ), ← hcl, upperBounds_closure] exact hBdd -
sSup_image_strictCell_eq_weakCelltheorem — Given a nonempty strict cell, a continuous real objective, and an upper bound for its strict-cell image, the strict and weak image sets have the same supremum.Proof (Lean source)
theorem sSup_image_strictCell_eq_weakCell {n : ℕ} {Γ : AffineSystem n} {φ : (Fin n → ℝ) → ℝ} (hΓ : (strictCell Γ).Nonempty) (hφ : Continuous φ) (hBdd : BddAbove (φ '' strictCell Γ)) : sSup (φ '' strictCell Γ) = sSup (φ '' weakCell Γ) := by have hcl := closure_image_strictCell_eq_closure_image_weakCell hΓ hφ have hub : upperBounds (φ '' strictCell Γ) = upperBounds (φ '' weakCell Γ) := by rw [← upperBounds_closure (φ '' strictCell Γ), hcl, upperBounds_closure] have hBdd' := bddAbove_image_weakCell_of_strictCell hΓ hφ hBdd have hne : (φ '' strictCell Γ).Nonempty := hΓ.image φ have hne' : (φ '' weakCell Γ).Nonempty := hne.mono (image_mono (strictCell_subset_weakCell Γ)) rw [← csInf_upperBounds_eq_csSup hBdd hne, ← csInf_upperBounds_eq_csSup hBdd' hne', hub] -
sInf_affineEval_strictCell_eq_weakCelltheorem — Given an affine objective, a nonempty strict cell, and a lower bound for the strict-cell objective image, the affine objective has the same infimum on the strict cell and weak relaxation.hypothesesconclusionProof (Lean source)
theorem sInf_affineEval_strictCell_eq_weakCell {n : ℕ} {Γ : AffineSystem n} (f : AffineFn n) (hΓ : (strictCell Γ).Nonempty) (hBdd : BddBelow (f.eval '' strictCell Γ)) : sInf (f.eval '' strictCell Γ) = sInf (f.eval '' weakCell Γ) := by exact sInf_image_strictCell_eq_weakCell hΓ f.continuous_eval hBdd -
sSup_affineEval_strictCell_eq_weakCelltheorem — Given an affine objective, a nonempty strict cell, and an upper bound for the strict-cell objective image, the affine objective has the same supremum on the strict cell and weak relaxation.hypothesesconclusionProof (Lean source)
theorem sSup_affineEval_strictCell_eq_weakCell {n : ℕ} {Γ : AffineSystem n} (f : AffineFn n) (hΓ : (strictCell Γ).Nonempty) (hBdd : BddAbove (f.eval '' strictCell Γ)) : sSup (f.eval '' strictCell Γ) = sSup (f.eval '' weakCell Γ) := by exact sSup_image_strictCell_eq_weakCell hΓ f.continuous_eval hBdd
Polynomial 7 core · 2 supporting This module compiles checked real multivariate polynomials of total degree at most one into the explicit affine-constraint representation and proves that this compilation preserves both strict and weak cells. ★ affineFnOfMvPolynomial_eval
Degree-one polynomial bridge
This module compiles checked real multivariate polynomials of total degree at most one into the explicit affine-constraint representation and proves that this compilation preserves both strict and weak cells.
def affineFnOfMvPolynomial reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a real multivariate polynomial, its compiled affine function is given by the coefficients of its degree-one monomials and its constant coefficient.
Definition (Lean source)
theorem affineFnOfMvPolynomial_eval reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a real multivariate polynomial, a proof that its total degree is at most one, and a coordinate vector, evaluating its compiled affine function equals evaluating the polynomial.
Formal statement
hypotheses
conclusion
(affineFnOfMvPolynomial p).eval x = eval x p
Proof (Lean source)
theorem affineFnOfMvPolynomial_eval {n : ℕ} (p : MvPolynomial (Fin n) ℝ)
(hp : p.totalDegree ≤ 1) (x : Fin n → ℝ) :
(affineFnOfMvPolynomial p).eval x = eval x p := by
classical
have hp_eq : p = C (coeff 0 p) +
∑ i, C (coeff (Finsupp.single i 1) p) * X i := by
ext d
by_cases hd0 : d = 0
· subst d
rw [MvPolynomial.coeff_add, MvPolynomial.coeff_C, coeff_linear_sum_zero]
simp
by_cases hd1 : ∃ i, d = Finsupp.single i 1
· obtain ⟨i, rfl⟩ := hd1
rw [MvPolynomial.coeff_add, MvPolynomial.coeff_C, coeff_linear_sum_single]
have hs : (0 : Fin n →₀ ℕ) ≠ Finsupp.single i 1 :=
Ne.symm (Finsupp.single_ne_zero.mpr one_ne_zero)
simp [hs]
· have hd_not_mem : d ∉ p.support := by
intro hd_mem
have hsum : d.sum (fun _ e => e) ≤ 1 := (MvPolynomial.le_totalDegree hd_mem).trans hp
exact (finsupp_eq_zero_or_single_of_sum_le_one d hsum).elim hd0 hd1
rw [MvPolynomial.notMem_support_iff.mp hd_not_mem, MvPolynomial.coeff_add,
MvPolynomial.coeff_C]
simp only [if_neg (Ne.symm hd0), zero_add]
rw [MvPolynomial.coeff_sum]
symm
apply Finset.sum_eq_zero
intro i hi
have hs : Finsupp.single i 1 ≠ d := fun h => hd1 ⟨i, h.symm⟩
simp [MvPolynomial.coeff_C_mul, MvPolynomial.coeff_X, hs]
unfold AffineFn.eval affineFnOfMvPolynomial
calc
(∑ i, coeff (Finsupp.single i 1) p * x i) + coeff 0 p =
coeff 0 p + ∑ i, coeff (Finsupp.single i 1) p * x i := add_comm _ _
_ = eval x (C (coeff 0 p) +
∑ i, C (coeff (Finsupp.single i 1) p) * X i) := by simp
_ = eval x p := by rw [← hp_eq]
structure PolynomialConstraint reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite number of coordinates, a checked polynomial constraint contains its polynomial left-hand side, its weak-or-strict mark, and a certificate that it is affine.
Definition (Lean source)
parameters
n :
ℕ
fields
The polynomial left-hand side, normalized against zero.
polynomial :
MvPolynomial (Fin n) ℝ
Whether the normalized inequality is weak or strict.
kind :
The polynomial has total degree at most one.
degree_le_one :
polynomial.totalDegree ≤ 1
def toConstraint reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell.PolynomialConstraint
Given a checked polynomial constraint, its affine constraint compilation is given by the compiled affine function with the original mark retained.
Definition (Lean source)
parameters
n :
ℕ
c :
def
def affineSystemOfPolynomials reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite list of checked polynomial constraints, its compiled affine system is given by compiling every listed constraint.
Definition (Lean source)
parameters
n :
ℕ
Γ :
def
given by
Γ.map PolynomialConstraint.toConstraint
def polynomialStrictCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite list of checked polynomial constraints, its direct strict polynomial cell is given by satisfaction of each original weak-or-strict polynomial comparison.
def polynomialWeakCell reviewed
⚑ flagged
Causalean.Mathlib.Optimization.Affine.SignCell
Given a finite list of checked polynomial constraints, its direct weak polynomial cell is given by weak satisfaction of every polynomial constraint.
Definition (Lean source)
2 supporting declarations (lemmas, instances)
-
strictCell_affineSystemOfPolynomialstheorem — Given a finite checked polynomial system, compilation preserves its strict cell.hypothesesn :ℕΓ :conclusionProof (Lean source)
theorem strictCell_affineSystemOfPolynomials {n : ℕ} (Γ : List (PolynomialConstraint n)) : strictCell (affineSystemOfPolynomials Γ) = polynomialStrictCell Γ := by ext x constructor · intro hx c hc have hmem : c.toConstraint ∈ affineSystemOfPolynomials Γ := List.mem_map.mpr ⟨c, hc, rfl⟩ have h := hx c.toConstraint hmem have hev := affineFnOfMvPolynomial_eval c.polynomial c.degree_le_one x cases hk : c.kind <;> simpa [polynomialStrictCell, Constraint.strictHolds, PolynomialConstraint.toConstraint, hk, hev] using h · intro hx c hc obtain ⟨d, hd, rfl⟩ := List.mem_map.mp hc have h := hx d hd have hev := affineFnOfMvPolynomial_eval d.polynomial d.degree_le_one x cases hk : d.kind <;> simpa [polynomialStrictCell, Constraint.strictHolds, PolynomialConstraint.toConstraint, hk, hev] using h -
weakCell_affineSystemOfPolynomialstheorem — Given a finite checked polynomial system, compilation preserves its weak cell.hypothesesn :ℕΓ :conclusionProof (Lean source)
theorem weakCell_affineSystemOfPolynomials {n : ℕ} (Γ : List (PolynomialConstraint n)) : weakCell (affineSystemOfPolynomials Γ) = polynomialWeakCell Γ := by ext x constructor · intro hx c hc have hmem : c.toConstraint ∈ affineSystemOfPolynomials Γ := List.mem_map.mpr ⟨c, hc, rfl⟩ have h := hx c.toConstraint hmem simpa [polynomialWeakCell, Constraint.weakHolds, PolynomialConstraint.toConstraint, affineFnOfMvPolynomial_eval c.polynomial c.degree_le_one x] using h · intro hx c hc obtain ⟨d, hd, rfl⟩ := List.mem_map.mp hc have h := hx d hd simpa [polynomialWeakCell, Constraint.weakHolds, PolynomialConstraint.toConstraint, affineFnOfMvPolynomial_eval d.polynomial d.degree_le_one x] using h