def StrictlyPositive {Q : Type u} (f : Q → ℝ) : Prop

A real-valued function on Q is strictly positive when all of its values are positive.

theorem StrictlyPositive.apply {Q : Type u} {f : Q → ℝ} (hf : StrictlyPositive f) (x : Q) : 0 < f x

A strictly positive function has positive value at every feasible point.

structure StrictlyPositiveObjectiveMinimizationProblem (Q : Type u) : Type u

Definition 7.85: a general minimization problem with strictly positive objective consists of a feasible type Q, a strictly positive objective function φ : Q → ℝ, and a chosen optimal solution x⋆ : Q minimizing φ over all feasible points.

• objective : Q → ℝ

  The objective function φ : Q → ℝ.

• objective_strictlyPositive : StrictlyPositive self.objective

  The objective function is strictly positive on the feasible set Q.

• optimalSolution : Q

  The chosen optimal solution x⋆ ∈ Q.

• optimalSolution_isMin : IsMinOn self.objective Set.univ self.optimalSolution

  The chosen optimal solution minimizes φ over the whole feasible set Q.

@[implicit_reducible]

instance instCoeFunStrictlyPositiveObjectiveMinimizationProblemForallReal {Q : Type u} : CoeFun (StrictlyPositiveObjectiveMinimizationProblem Q) fun (x : StrictlyPositiveObjectiveMinimizationProblem Q) => Q → ℝ

A strictly-positive-objective minimization problem can be used as its objective function.

def StrictlyPositiveObjectiveMinimizationProblem.toSetConstrainedMinimizationProblem {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : SetConstrainedMinimizationProblem Q

The canonical Chapter 1 whole-space minimization owner attached to the objective.

@[simp]

theorem StrictlyPositiveObjectiveMinimizationProblem.toSetConstrainedMinimizationProblem_feasibleSet {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : problem.toSetConstrainedMinimizationProblem.feasibleSet = Set.univ

@[simp]

theorem StrictlyPositiveObjectiveMinimizationProblem.toSetConstrainedMinimizationProblem_apply {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) (x : Q) : problem.toSetConstrainedMinimizationProblem.objective x = problem.objective x

def StrictlyPositiveObjectiveMinimizationProblem.optimalValue {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : ℝ

The optimal value φ⋆ is the objective value at the chosen optimal solution.

theorem StrictlyPositiveObjectiveMinimizationProblem.optimalValue_eq_sInf_range {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : problem.optimalValue = sInf (Set.range problem.objective)

Expanding optimalValue gives the infimum of the objective values attained on Q.

@[simp]

theorem StrictlyPositiveObjectiveMinimizationProblem.optimalValue_eq_objective_optimalSolution {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : problem.optimalValue = problem.objective problem.optimalSolution

The optimal value is attained at the chosen optimal solution x⋆.

@[simp]

theorem StrictlyPositiveObjectiveMinimizationProblem.toSetConstrainedMinimizationProblem_optimalValue {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : problem.toSetConstrainedMinimizationProblem.optimalValue = ↑problem.optimalValue

The Chapter 1 owner optimal value agrees with the source-facing optimal value.

theorem StrictlyPositiveObjectiveMinimizationProblem.objective_optimalSolution_pos {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : 0 < problem.objective problem.optimalSolution

The chosen optimal solution has strictly positive objective value.

theorem StrictlyPositiveObjectiveMinimizationProblem.optimalValue_pos {Q : Type u} (problem : StrictlyPositiveObjectiveMinimizationProblem Q) : 0 < problem.optimalValue

The optimal value is strictly positive.