def IsAbsoluteAccuracyApproximateSolutionOn {X : Type u} (Q : Set X) (phi : X → ℝ) (ε : ℝ) (xBar : X) : Prop

Definition 7.93: a point xBar is an absolute-accuracy ε-approximate solution for the minimization of phi over the feasible set Q when ε > 0 and xBar is an ε-approximate minimizer for the Chapter 1 constrained-minimization owner on (Q, phi).

theorem IsAbsoluteAccuracyApproximateSolutionOn.epsilon_pos {X : Type u} {Q : Set X} {phi : X → ℝ} {ε : ℝ} {xBar : X} (h : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar) : 0 < ε

The absolute-accuracy parameter of an absolute-accuracy approximate solution is positive.

theorem IsAbsoluteAccuracyApproximateSolutionOn.isApproximateMinimizer {X : Type u} {Q : Set X} {phi : X → ℝ} {ε : ℝ} {xBar : X} (h : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar) : { feasibleSet := Q, objective := phi }.IsApproximateMinimizer ε xBar

An absolute-accuracy approximate solution is an approximate minimizer for the canonical Chapter 1 constrained-minimization owner on (Q, phi).

theorem IsAbsoluteAccuracyApproximateSolutionOn.feasible {X : Type u} {Q : Set X} {phi : X → ℝ} {ε : ℝ} {xBar : X} (h : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar) : xBar ∈ Q

An absolute-accuracy approximate solution is feasible for the original constrained problem.

theorem IsAbsoluteAccuracyApproximateSolutionOn.objective_le {X : Type u} {Q : Set X} {phi : X → ℝ} {ε : ℝ} {xBar : X} (h : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar) : ↑(phi xBar) ≤ { feasibleSet := Q, objective := phi }.optimalValue + ↑ε

An absolute-accuracy approximate solution satisfies the defining owner-valued additive objective bound.

theorem IsAbsoluteAccuracyApproximateSolutionOn.optimalValue_eq_coe_sInf {X : Type u} {Q : Set X} {phi : X → ℝ} (hQ : Q.Nonempty) (hbounded : BddBelow (phi '' Q)) : { feasibleSet := Q, objective := phi }.optimalValue = ↑(sInf (phi '' Q))

If the feasible objective values are nonempty and bounded below, then the Chapter 1 owner optimal value agrees with the textbook real infimum.

theorem IsAbsoluteAccuracyApproximateSolutionOn.optimalValue_toReal_eq_sInf {X : Type u} {Q : Set X} {phi : X → ℝ} (hQ : Q.Nonempty) (hbounded : BddBelow (phi '' Q)) : { feasibleSet := Q, objective := phi }.optimalValue.toReal = sInf (phi '' Q)

If the feasible objective values are nonempty and bounded below, then the owner optimal value has the textbook real infimum as its toReal.

theorem IsAbsoluteAccuracyApproximateSolutionOn.objective_le_sInf_add {X : Type u} {Q : Set X} {phi : X → ℝ} {ε : ℝ} {xBar : X} (h : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar) (hbounded : BddBelow (phi '' Q)) : phi xBar ≤ sInf (phi '' Q) + ε

If the feasible objective values are bounded below, then the owner-valued additive bound in Definition 7.93 recovers the textbook real inequality against sInf (phi '' Q).

theorem IsAbsoluteAccuracyApproximateSolutionOn.iff_epsilon_pos_and_feasible_and_objective_le_sInf_add {X : Type u} {Q : Set X} {phi : X → ℝ} {ε : ℝ} {xBar : X} (hbounded : BddBelow (phi '' Q)) : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar ↔ 0 < ε ∧ xBar ∈ Q ∧ phi xBar ≤ sInf (phi '' Q) + ε

If the feasible objective values are bounded below, then Definition 7.93 is equivalent to the textbook positive-ε additive objective-gap inequality.

theorem isAbsoluteAccuracyApproximateSolutionOn_iff {X : Type u} (Q : Set X) (phi : X → ℝ) (ε : ℝ) (xBar : X) : IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar ↔ 0 < ε ∧ { feasibleSet := Q, objective := phi }.IsApproximateMinimizer ε xBar

Unfolding IsAbsoluteAccuracyApproximateSolutionOn Q phi ε xBar gives positivity of ε together with the canonical Chapter 1 approximate-minimizer owner on (Q, phi).