@[reducible, inline]

abbrev levelMethodApproximateProblem {α : Type u} (Q : Set α) (model : ℕ → α → ℝ) (k : ℕ) : SetConstrainedMinimizationProblem α

The exact constrained model problem at step k, obtained by minimizing the model x ↦ model k x over the feasible set Q.

noncomputable def levelMethodHistoryFromApproximateValues {α : Type u} (approximateOptimalValue : ℕ → ℝ) (f : α → ℝ) (xSeq : ℕ → α) : LevelMethodHistory

Explicit real scalar history attached to prescribed lower values \hat f_k^* and sampled objective values. The mathematically faithful exact lower values remain the canonical EReal owners (levelMethodApproximateProblem Q model k).optimalValue; this constructor is only the real-history bridge used once those lower values have been supplied explicitly.

theorem levelMethodHistoryFromApproximateValues_approximateOptimalValue_eq {α : Type u} (approximateOptimalValue : ℕ → ℝ) (f : α → ℝ) (xSeq : ℕ → α) (k : ℕ) : (levelMethodHistoryFromApproximateValues approximateOptimalValue f xSeq).approximateOptimalValue k = approximateOptimalValue k

The lower coordinate of levelMethodHistoryFromApproximateValues is the supplied real lower value.

theorem levelMethodHistoryFromApproximateValues_optimalValue_eq {α : Type u} (approximateOptimalValue : ℕ → ℝ) (f : α → ℝ) (xSeq : ℕ → α) (k : ℕ) : (levelMethodHistoryFromApproximateValues approximateOptimalValue f xSeq).optimalValue k = bestFunctionValueUpTo (fun (i : ℕ) => f (xSeq i)) k

theorem levelMethodHistoryFromApproximateValues_approximateOptimalValue_eq_optimalValue {α : Type u} (Q : Set α) (model : ℕ → α → ℝ) (hatf : ℕ → ℝ) (f : α → ℝ) (xSeq : ℕ → α) (hhat : ∀ (k : ℕ), ↑(hatf k) = (levelMethodApproximateProblem Q model k).optimalValue) (k : ℕ) : ↑((levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue k) = (levelMethodApproximateProblem Q model k).optimalValue

If the supplied real lower values are exact, then the lower coordinate of levelMethodHistoryFromApproximateValues agrees with the canonical EReal model minimum.

theorem levelMethodHistoryFromAttainedApproximateValues_approximateOptimalValue_eq_optimalValue {α : Type u} (Q : Set α) (model : ℕ → α → ℝ) (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (k : ℕ), xHat k ∈ Q) (hxHat_min : ∀ (k : ℕ), IsMinOn (model k) Q (xHat k)) (k : ℕ) : ↑((levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue k) = (levelMethodApproximateProblem Q model k).optimalValue

The attained-minimum specialization of levelMethodHistoryFromApproximateValues agrees with the canonical EReal lower-value owner at each step, provided the chosen sequence xHat really minimizes each model on Q.

theorem levelMethodApproximateProblem_optimalValue_mono_of_pointwiseModelMono {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodApproximateProblem Q model k).optimalValue ≤ (levelMethodApproximateProblem Q model (k + 1)).optimalValue

Pointwise monotonicity of the model family makes the canonical exact lower values monotone.

theorem levelMethodApproximateProblem_optimalValue_le_bestFunctionValueUpTo_of_underestimator {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq : ℕ → α) (hxSeq : ∀ (k : ℕ), xSeq k ∈ Q) (hunder : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ f x) (k : ℕ) : (levelMethodApproximateProblem Q model k).optimalValue ≤ ↑(bestFunctionValueUpTo (fun (i : ℕ) => f (xSeq i)) k)

If every model is an underestimator on Q, then each canonical exact lower value is bounded above by the best sampled objective value. This is stated first on the faithful EReal owner.

theorem levelMethodApproximateProblem_optimalValue_stepwiseBounds_of_monotoneUnderestimators {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq : ℕ → α) (hxSeq : ∀ (k : ℕ), xSeq k ∈ Q) (hunder : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ f x) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodApproximateProblem Q model k).optimalValue ≤ (levelMethodApproximateProblem Q model (k + 1)).optimalValue ∧ (levelMethodApproximateProblem Q model (k + 1)).optimalValue ≤ ↑(bestFunctionValueUpTo (fun (i : ℕ) => f (xSeq i)) (k + 1)) ∧ ↑(bestFunctionValueUpTo (fun (i : ℕ) => f (xSeq i)) (k + 1)) ≤ ↑(bestFunctionValueUpTo (fun (i : ℕ) => f (xSeq i)) k)

Proposition 3.50, canonical form: the source-faithful stepwise order chain is stated on the exact lower-value owner in EReal, so no extra attainment hypothesis is needed to express the model lower values faithfully.

theorem levelMethodHistoryFromApproximateValues_approximateOptimalValue_mono_of_pointwiseModelMono {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq : ℕ → α) (hatf : ℕ → ℝ) (hhat : ∀ (j : ℕ), ↑(hatf j) = (levelMethodApproximateProblem Q model j).optimalValue) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue k ≤ (levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue (k + 1)

Under the exactness certificate hhat, pointwise monotonicity of the model family makes the explicit real lower coordinates monotone.

theorem levelMethodHistoryFromApproximateValues_fhat_le_fstar_of_underestimator {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq : ℕ → α) (hatf : ℕ → ℝ) (hhat : ∀ (j : ℕ), ↑(hatf j) = (levelMethodApproximateProblem Q model j).optimalValue) (hxSeq : ∀ (k : ℕ), xSeq k ∈ Q) (hunder : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ f x) (k : ℕ) : (levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue k ≤ (levelMethodHistoryFromApproximateValues hatf f xSeq).optimalValue k

Under the exactness certificate hhat, every model underestimator is bounded above by the best sampled objective value in the explicit real history.

theorem levelMethodHistoryFromApproximateValues_stepwiseBounds_of_monotoneUnderestimators {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq : ℕ → α) (hatf : ℕ → ℝ) (hhat : ∀ (j : ℕ), ↑(hatf j) = (levelMethodApproximateProblem Q model j).optimalValue) (hxSeq : ∀ (k : ℕ), xSeq k ∈ Q) (hunder : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ f x) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue k ≤ (levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue (k + 1) ∧ (levelMethodHistoryFromApproximateValues hatf f xSeq).approximateOptimalValue (k + 1) ≤ (levelMethodHistoryFromApproximateValues hatf f xSeq).optimalValue (k + 1) ∧ (levelMethodHistoryFromApproximateValues hatf f xSeq).optimalValue (k + 1) ≤ (levelMethodHistoryFromApproximateValues hatf f xSeq).optimalValue k

Proposition 3.50, source-facing real-history form: if the supplied lower values are exact, then the textbook chain \hat f_k^* ≤ \hat f_{k+1}^* ≤ f_{k+1}^* ≤ f_k^* holds for levelMethodHistoryFromApproximateValues hatf f xSeq.

theorem attainedApproximateOptimalValue_mono_of_pointwiseModelMono {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (j : ℕ), xHat j ∈ Q) (hxHat_min : ∀ (j : ℕ), IsMinOn (model j) Q (xHat j)) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue k ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue (k + 1)

Companion bridge: under an explicit minimizing sequence xHat, pointwise monotonicity of the model family makes the attained real lower coordinates monotone.

theorem attainedApproximateOptimalValue_le_optimalValue_of_underestimator {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (j : ℕ), xHat j ∈ Q) (hxHat_min : ∀ (j : ℕ), IsMinOn (model j) Q (xHat j)) (hxSeq : ∀ (k : ℕ), xSeq k ∈ Q) (hunder : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ f x) (k : ℕ) : (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue k ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).optimalValue k

Companion bridge: under an explicit minimizing sequence xHat, every model underestimator is bounded above by the best sampled objective value in the attained real history.

theorem attainedValueInterval_subset_step_of_pointwiseModelMono {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (j : ℕ), xHat j ∈ Q) (hxHat_min : ∀ (j : ℕ), IsMinOn (model j) Q (xHat j)) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).valueInterval (k + 1) ⊆ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).valueInterval k

Companion bridge: under an explicit minimizing sequence xHat, the interval inclusion Δ_{k+1} ⊆ Δ_k follows from pointwise monotonicity of the models. The underestimator hypothesis from the textbook is redundant for this conclusion.

theorem attainedGap_antitone_step_of_pointwiseModelMono {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (j : ℕ), xHat j ∈ Q) (hxHat_min : ∀ (j : ℕ), IsMinOn (model j) Q (xHat j)) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).gap (k + 1) ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).gap k

Companion bridge: under an explicit minimizing sequence xHat, the level-method gap δ_k = f_k^* - \hat f_k^* decreases from step k to step k + 1 under pointwise monotone models. The underestimator hypothesis is redundant for this conclusion.

theorem attainedLevelMethodValueInterval_subset_and_gap_antitone_of_pointwiseModelMono {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (j : ℕ), xHat j ∈ Q) (hxHat_min : ∀ (j : ℕ), IsMinOn (model j) Q (xHat j)) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).valueInterval (k + 1) ⊆ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).valueInterval k ∧ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).gap (k + 1) ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).gap k

Companion bridge: under an explicit minimizing sequence xHat, pointwise monotonicity of the models makes the attained-history intervals nested downward and the attained-history gaps nonincreasing.

theorem attainedLevelMethodStepwiseBounds_of_monotoneUnderestimators {α : Type u} {Q : Set α} {model : ℕ → α → ℝ} (f : α → ℝ) (xSeq xHat : ℕ → α) (hxHat_mem : ∀ (j : ℕ), xHat j ∈ Q) (hxHat_min : ∀ (j : ℕ), IsMinOn (model j) Q (xHat j)) (hxSeq : ∀ (k : ℕ), xSeq k ∈ Q) (hunder : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ f x) (hmono : ∀ (k : ℕ), ∀ x ∈ Q, model k x ≤ model (k + 1) x) (k : ℕ) : (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue k ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue (k + 1) ∧ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).approximateOptimalValue (k + 1) ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).optimalValue (k + 1) ∧ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).optimalValue (k + 1) ≤ (levelMethodHistoryFromApproximateValues (fun (i : ℕ) => model i (xHat i)) f xSeq).optimalValue k

Companion bridge: under an explicit minimizing sequence xHat, the textbook real chain \hat f_k^* ≤ \hat f_{k+1}^* ≤ f_{k+1}^* ≤ f_k^* follows from the canonical EReal Proposition 3.50 theorem.