theorem associated_ellipsoid_volume_decay_real {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) : 1 < n → (∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) → (∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) → ∀ (hR : 0 ≤ R) (k : ℕ), (MeasureTheory.volume (EllipsoidMethod.associatedEllipsoid problem sorry R k)).toReal ≤ (1 - 1 / (↑n + 1) ^ 2).rpow (↑(k * n) / 2) * (MeasureTheory.volume (Metric.closedBall initialCenter R)).toReal

Helper for Proposition 3.47: the associated ellipsoid volumes decay geometrically along the ellipsoid recursion, relative to the initial radius-R ball.

theorem associated_ellipsoid_volume_decay_ennreal {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) : 1 < n → (∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) → (∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) → ∀ (hR : 0 ≤ R) (k : ℕ), MeasureTheory.volume (EllipsoidMethod.associatedEllipsoid problem sorry R k) ≤ ENNReal.ofReal ((1 - 1 / (↑n + 1) ^ 2).rpow (↑(k * n) / 2)) * MeasureTheory.volume (Metric.closedBall initialCenter R)

Helper for Proposition 3.47: the same geometric ellipsoid-volume decay can be stated directly in the ENNReal form required by Proposition 3.45.

theorem accuracy_budget_implies_next_stage_log_threshold {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} : 0 < ε → ε ≤ ↑M * R → ∀ (hρ : 0 < ρ) (hN : 2 * ↑(n + 1) ^ 2 * Real.log (↑M * R ^ 2 / (ρ * ε)) ≤ ↑N), 2 * ↑(n + 1) ^ 2 * Real.log (↑M * R ^ 2 / (ρ * ε)) < ↑N + 1 ∧ R * (R / ρ * Real.exp (-((↑N + 1) / (2 * (↑n + 1) ^ 2)))) < ε / ↑M

Helper for Proposition 3.47: the accuracy budget forces the strict next-stage logarithmic threshold and the final scalar decay estimate used to reach ε / M.

theorem log_threshold_of_accuracy_budget_for_outer_radius {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} : 0 < ε → ε ≤ ↑M * R → ∀ (hρ : 0 < ρ) (hN : 2 * ↑(n + 1) ^ 2 * Real.log (↑M * R ^ 2 / (ρ * ε)) ≤ ↑N), 2 * ↑(n + 1) ^ 2 * Real.log (R / ρ) < ↑N + 1

Helper for Proposition 3.47: the accuracy budget already implies the weaker logarithmic threshold log (R / ρ) needed by Proposition 3.45.

theorem selected_feasible_count_pos_of_accuracy_budget {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} : 0 < ε → ε ≤ ↑M * R → problem.feasibleSet.SatisfiesInteriorBallCondition ρ → problem.feasibleSet ⊆ Metric.closedBall sorry R → 1 < n → (∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) → (∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) → problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0 → ∀ (hN : 2 * ↑(n + 1) ^ 2 * Real.log (↑M * R ^ 2 / (ρ * ε)) ≤ ↑N), 0 < Nat.count (fun (j : ℕ) => EllipsoidMethod.center problem sorry R j ∈ problem.feasibleSet) (N + 1)

Helper for Proposition 3.47: the same budget already guarantees a positive selected-feasible count among the first N + 1 ellipsoid centers.

theorem localization_measure_le_of_mem_closedBall {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) (xRef : EuclideanSpace ℝ (Fin n)) {x : EuclideanSpace ℝ (Fin n)} (hx : x ∈ Metric.closedBall xRef R) : subgradientLocalizationMeasure problem.oracle.oracle xRef x ≤ R

Helper for Proposition 3.47: every selected feasible sample among the first N + 1 queries lies in the radius-R outer ball around xStar, so its pointwise localization measure is at most R.

theorem selected_point_localization_measure_le_outer_radius {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} (j : Fin (Nat.count (fun (t : ℕ) => EllipsoidMethod.center problem sorry R t ∈ problem.feasibleSet) (N + 1))) : subgradientLocalizationMeasure problem.oracle.oracle sorry (feasibleSubsequence problem.feasibleSet (EllipsoidMethod.center problem sorry R) ↑j) ≤ R

Helper for Proposition 3.47: every selected feasible sample among the first N + 1 queries lies in the radius-R outer ball around xStar, so its pointwise localization measure is at most R.

theorem selected_best_value_witness_is_approximate_minimizer {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} (hm : 0 < Nat.count (fun (j : ℕ) => EllipsoidMethod.center problem sorry R j ∈ problem.feasibleSet) (N + 1)) (hbest : ↑(bestFunctionValueUpTo (problem.objective ∘ feasibleSubsequence problem.feasibleSet (EllipsoidMethod.center problem sorry R)) (Nat.count (fun (j : ℕ) => EllipsoidMethod.center problem sorry R j ∈ problem.feasibleSet) (N + 1) - 1)) ≤ problem.optimalValue + ↑ε) : ∃ k ≤ N, problem.IsApproximateMinimizer ε (EllipsoidMethod.center problem sorry R k)

Helper for Proposition 3.47: a selected feasible sample whose value realizes the canonical best sampled prefix value yields the required raw queried center witness.

theorem ellipsoid_method_oracle_complexity_of_interior_ball_bestFunctionValueUpTo {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} (hN : 2 * ↑(n + 1) ^ 2 * Real.log (↑M * R ^ 2 / (ρ * ε)) ≤ ↑N) : ↑(bestFunctionValueUpTo (problem.objective ∘ feasibleSubsequence problem.feasibleSet (EllipsoidMethod.center problem sorry R)) (Nat.count (fun (j : ℕ) => EllipsoidMethod.center problem sorry R j ∈ problem.feasibleSet) (N + 1) - 1)) ≤ problem.optimalValue + ↑ε

Companion owner theorem for Proposition 3.47: under the same hypotheses, the canonical best sampled value along the selected feasible subsequence of queried centers in the first N + 1 queries is at most ε above the canonical constrained optimum problem.optimalValue. The positivity of the selected-feasible prefix now follows from the same accuracy budget after the small-accuracy bridge ε ≤ (M : ℝ) * R, and is not kept as a separate public premise.

theorem ellipsoid_method_oracle_complexity_of_interior_ball {n : ℕ} (problem : ConvexMinimizationWithSeparationOracle (EuclideanSpace ℝ (Fin n))) (initialCenter : EuclideanSpace ℝ (Fin sorry)) (xStar : EuclideanSpace ℝ (Fin sorry)) (M : NNReal) {R ρ ε : ℝ} (hε : 0 < ε) (hε_le : ε ≤ ↑M * R) (hf_lipschitz : LipschitzOnWith M problem.objective (Metric.closedBall sorry R)) (hfeasible_ball : problem.feasibleSet.SatisfiesInteriorBallCondition ρ) (hxStar : sorry) (hfeasible_subset_ball : problem.feasibleSet ⊆ Metric.closedBall sorry R) (hn : 1 < n) (hcut_nonzero : ∀ (k : ℕ), EllipsoidMethod.cuttingVector problem sorry R k ≠ 0) (hshape_pos : ∀ (k : ℕ), (EllipsoidMethod.shape problem sorry R k).PosDef) (hE0_cover : problem.feasibleSet ⊆ EllipsoidMethod.associatedEllipsoid problem sorry R 0) {N : ℕ} (hN : 2 * ↑(n + 1) ^ 2 * Real.log (↑M * R ^ 2 / (ρ * ε)) ≤ ↑N) : ∃ k ≤ N, problem.IsApproximateMinimizer ε (EllipsoidMethod.center problem sorry R k)

Proposition 3.47 in source-facing form: under the logarithmic oracle budget, one of the queried ellipsoid centers is an ε-approximate minimizer of the constrained problem.