Fixed YTM convergence ingredients

This file is the fixed part obtained after merging the old v126 and v127 interface. It exposes the Newton direction, the fixed predictor step, the local predictor/corrector guarantees, and the contraction/log-bound lemmas used by the algorithm-level proof.

It deliberately does not contain a user-supplied sequence w : Nat → HSState n. That older interface was removed because the generated-algorithm interface in GeneratedConvergence.lean constructs the iterates recursively and makes the algorithm dependency clearer.

Lean tactic reading guide for this file

The mathematical content below is the YTM local analysis. The short Lean tactics used in the proofs have the following roles.

• intro h turns a goal of the form P → Q into the new assumption h : P and the remaining goal Q. For ∀ x, ..., it introduces the quantified variable.
• have h : P := by ... proves an intermediate mathematical fact and gives it the name h for later use.
• rcases h with ⟨h1, h2, ...⟩ decomposes a conjunction or existential proof. It corresponds to unpacking the components of a theorem such as 0 < α ∧ α ≤ 1 ∧ ....
• simp only [...] rewrites only by the listed definitions and lemmas. This is safer than unrestricted simp, because a later change in the imported library is less likely to change the proof.
• simpa [defs] using h means: simplify the current goal and the type of h using defs, then use h. Most occurrences here only unfold names such as ytmPredictorAlpha or remove a harmless 1 - 0.
• ring proves polynomial identities over real numbers, for example rearranging (1 - a * (1 - 0)) into 1 - a.
• linarith proves linear inequalities from the hypotheses. It is used only when the remaining goal is linear in the real variables.
• nlinarith is the nonlinear version, used when products such as hdim n * ε or squares appear.
• field_simp [h₁, h₂] clears denominators using the supplied nonzero proofs; this is used only for algebraic cancellation in positive denominators.

Predictor scaled-direction algebra for the remaining v106 obligation

theorem HSDInteriorPointLP.predictor_component_quotient_sum_eq_neg_one {n : ℕ} (w : HSState n) (d : HSDirection n) (hinterior : Interior w) (hdir : HSDStepDirection w d 0) (i : Fin n) : d.dx i / w.x i + d.ds i / w.s i = -1

Step 1, vector part: the predictor complementarity equation in quotient form.

theorem HSDInteriorPointLP.predictor_scalar_quotient_sum_eq_neg_one {n : ℕ} (w : HSState n) (d : HSDirection n) (hinterior : Interior w) (hdir : HSDStepDirection w d 0) : d.dtau / w.tau + d.dkappa / w.kappa = -1

Step 1, scalar part: the predictor scalar complementarity equation in quotient form.

theorem HSDInteriorPointLP.predictor_quotient_weighted_cross_zero {n : ℕ} (w : HSState n) (d : HSDirection n) (hinterior : Interior w) (hdir : HSDStepDirection w d 0) : ∑ i : Fin n, w.x i * w.s i * (d.dx i / w.x i) * (d.ds i / w.s i) + w.tau * w.kappa * (d.dtau / w.tau) * (d.dkappa / w.kappa) = 0

Step 2: skew orthogonality rewritten in quotient variables.

theorem HSDInteriorPointLP.complementarity_total_eq_hdim_mul_mu {n : ℕ} (w : HSState n) : ∑ i : Fin n, w.x i * w.s i + w.tau * w.kappa = hdim n * mu w

Step 3: the total complementarity product is hdim n * mu w.

theorem HSDInteriorPointLP.square_sum_eq_one_sub_two_mul_of_sum_eq_neg_one {u v : ℝ} (h : u + v = -1) : u ^ 2 + v ^ 2 = 1 - 2 * (u * v)

Algebraic identity from u + v = -1: it is used componentwise in Step 4.

theorem HSDInteriorPointLP.predictor_weighted_relative_norm_identity {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : ∑ i : Fin n, w.x i * w.s i * ((d.dx i / w.x i) ^ 2 + (d.ds i / w.s i) ^ 2) + w.tau * w.kappa * ((d.dtau / w.tau) ^ 2 + (d.dkappa / w.kappa) ^ 2) = hdim n * mu w

Step 4: weighted norm identity for predictor quotient variables.

theorem HSDInteriorPointLP.neighborhood_component_product_lower_tight {n : ℕ} (w : HSState n) (hneigh : HSDNeighborhood ytmBetaTight w) (i : Fin n) : 3 / 4 * mu w ≤ w.x i * w.s i

Step 5, vector part: tight-neighborhood lower bound 3μ/4 ≤ xᵢsᵢ.

theorem HSDInteriorPointLP.neighborhood_scalar_product_lower_tight {n : ℕ} (w : HSState n) (hneigh : HSDNeighborhood ytmBetaTight w) : 3 / 4 * mu w ≤ w.tau * w.kappa

Step 5, scalar part: tight-neighborhood lower bound 3μ/4 ≤ τκ.

theorem HSDInteriorPointLP.predictor_component_quotient_square_bounds {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) (i : Fin n) : (d.dx i / w.x i) ^ 2 ≤ 4 / 3 * hdim n ∧ (d.ds i / w.s i) ^ 2 ≤ 4 / 3 * hdim n

Step 6, vector part: the weighted identity gives componentwise quotient-square bounds.

theorem HSDInteriorPointLP.predictor_scalar_quotient_square_bounds {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : (d.dtau / w.tau) ^ 2 ≤ 4 / 3 * hdim n ∧ (d.dkappa / w.kappa) ^ 2 ≤ 4 / 3 * hdim n

Step 6, scalar part: quotient-square bounds for τ and κ.

theorem HSDInteriorPointLP.ytmStepConstant_le_half : ytmStepConstant ≤ 1 / 2

A convenient stronger numerical bound for the fixed YTM constant.

theorem HSDInteriorPointLP.predictor_fixed_alpha_sq_mul_hdim (n : ℕ) : predictorFixedAlpha n ^ 2 * hdim n = ytmStepConstant ^ 2

The fixed alpha cancels the homogenized dimension after squaring.

theorem HSDInteriorPointLP.predictor_fixed_alpha_sq_four_thirds_hdim_lt_one (n : ℕ) : predictorFixedAlpha n ^ 2 * (4 / 3 * hdim n) < 1

Step 7: fixed-alpha constant evaluation used by the scaled bounds.

theorem HSDInteriorPointLP.abs_alpha_mul_lt_one_of_square_bound (α u B : ℝ) (hu : u ^ 2 ≤ B) (hαB : α ^ 2 * B < 1) : |α * u| < 1

Step 8: square bound plus fixed-alpha constant bound gives an absolute bound.

Predictor center-bound estimates for Steps 9--12

theorem HSDInteriorPointLP.abs_mul_le_half_sq_add_sq (u v : ℝ) : |u * v| ≤ (u ^ 2 + v ^ 2) / 2

Elementary estimate |uv| ≤ (u² + v²)/2.

theorem HSDInteriorPointLP.predictor_second_order_l1_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : ∑ i : Fin n, |d.dx i * d.ds i| + |d.dtau * d.dkappa| ≤ hdim n * mu w / 2

Step 9, ℓ₁ version: the sum of absolute second-order predictor products is bounded by half of the weighted relative norm.

theorem HSDInteriorPointLP.predictor_second_order_square_sum_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : ∑ i : Fin n, (d.dx i * d.ds i) ^ 2 + (d.dtau * d.dkappa) ^ 2 ≤ (hdim n * mu w / 2) ^ 2

Step 9: second-order predictor products have the required square-sum bound.

theorem HSDInteriorPointLP.predictor_old_residual_square_sum_bound {n : ℕ} (w : HSState n) (hneigh : HSDNeighborhood ytmBetaTight w) : ∑ i : Fin n, (w.x i * w.s i - mu w) ^ 2 + (w.tau * w.kappa - mu w) ^ 2 ≤ (ytmBetaTight * mu w) ^ 2

The old centrality residual, in the sign convention used by the predictor residual, is bounded by the tight neighborhood radius.

theorem HSDInteriorPointLP.sq_add_le_two_sq_add_two_sq (x y : ℝ) : (x + y) ^ 2 ≤ 2 * x ^ 2 + 2 * y ^ 2

Pointwise two-term square inequality used as a square-sum version of the triangle estimate for Step 10.

theorem HSDInteriorPointLP.predictor_residual_split_square_sum_bound {n : ℕ} (a b : ℝ) (r q : Fin n → ℝ) (ρ η : ℝ) : ∑ i : Fin n, (a * r i + b * q i) ^ 2 + (a * ρ + b * η) ^ 2 ≤ 2 * a ^ 2 * (∑ i : Fin n, r i ^ 2 + ρ ^ 2) + 2 * b ^ 2 * (∑ i : Fin n, q i ^ 2 + η ^ 2)

Step 10/11: applying the two-term square estimate componentwise to the predictor residual split. This is a slightly stronger bookkeeping form than introducing a separate Euclidean norm object.

theorem HSDInteriorPointLP.predictor_fixed_alpha_le_half (n : ℕ) : predictorFixedAlpha n ≤ 1 / 2

The fixed predictor step length is at most one half.

theorem HSDInteriorPointLP.predictor_center_two_square_constant_bound {n : ℕ} (μ : ℝ) (_hμ : 0 ≤ μ) : 2 * (1 - predictorFixedAlpha n) ^ 2 * (ytmBetaTight * μ) ^ 2 + 2 * (predictorFixedAlpha n ^ 2) ^ 2 * (hdim n * μ / 2) ^ 2 ≤ (ytmBetaWide * ((1 - predictorFixedAlpha n) * μ)) ^ 2

Step 12: numerical constant evaluation for the center estimate, in the squared bookkeeping form used above.

theorem HSDInteriorPointLP.predictor_fixed_center_bound {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : ∑ i : Fin n, predictorVecResidualAfter w d i ^ 2 + predictorScalarResidualAfter w d ^ 2 ≤ (ytmBetaWide * ((1 - predictorFixedAlpha n) * mu w)) ^ 2

Steps 9--12 combined: the fixed predictor residual is inside the wide center radius.

Active predictor obligation after splitting fixed material

All already-fixed algebra and neighborhood bookkeeping have been moved to LocalNeighborhoodEstimates. This file starts with the only remaining analytic predictor estimate, followed by the small wrappers that turn it into the existing local-theory statements.

theorem HSDInteriorPointLP.YTM_predictor_fixed_scaled_core_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → PredictorFixedScaledCoreBounds w d

Remaining YTM scaled-norm estimate in named core form.

This is the single remaining analytic predictor obligation. Earlier shifted-square scaffolding was removed because it was not actually closing this estimate and made the file hard to maintain.

theorem HSDInteriorPointLP.YTM_predictor_fixed_scaled_norm_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → PredictorFixedScaledNormBounds w d

Expanded form of the remaining YTM scaled-norm estimate.

theorem HSDInteriorPointLP.YTM_predictor_fixed_scaled_direction_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → PredictorFixedScaledDirectionBounds w d

Remaining YTM scaled-direction estimate.

All algebraic consequences of the natural scaled-norm estimate are proved below without placeholders; this theorem only converts those scaled bounds into the existing relative-step package.

theorem HSDInteriorPointLP.YTM_predictor_fixed_relative_step_and_center_bound {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → (∀ (i : Fin n), |ytmStepConstant / √(hdim n) * d.dx i| < w.x i ∧ |ytmStepConstant / √(hdim n) * d.ds i| < w.s i) ∧ |ytmStepConstant / √(hdim n) * d.dtau| < w.tau ∧ |ytmStepConstant / √(hdim n) * d.dkappa| < w.kappa ∧ ∑ i : Fin n, ((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ^ 2 + ((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)) ^ 2 ≤ (ytmBetaWide * ((1 - ytmStepConstant / √(hdim n)) * mu w)) ^ 2

Remaining YTM scaled predictor estimate in relative-step form.

This is a sharper and more usable formulation of the remaining analytic input: the fixed predictor step is small relative to every positive component, and the explicit centrality residual is bounded by the 1/2 neighborhood radius. The relative bounds imply the cross-product lower bounds used above, so the only non-algebraic part left is now the standard YTM scaled-direction estimate.

theorem HSDInteriorPointLP.YTM_predictor_fixed_explicit_cross_lower_and_center_bound {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → (∀ (i : Fin n), -((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ∧ -((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa) ∧ ∑ i : Fin n, ((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ^ 2 + ((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa - mu w) + (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa)) ^ 2 ≤ (ytmBetaWide * ((1 - ytmStepConstant / √(hdim n)) * mu w)) ^ 2

Explicit fixed-step YTM predictor estimate.

This is the remaining analytic estimate written entirely in terms of the current point, the predictor direction, and the fixed step length. The surrounding lemmas convert this explicit estimate into product positivity and the N(1/2) center bound for addStep.

theorem HSDInteriorPointLP.YTM_predictor_fixed_cross_lower_and_center_bound {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → (∀ (i : Fin n), -((1 - ytmStepConstant / √(hdim n)) * (w.x i * w.s i)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dx i * d.ds i)) ∧ -((1 - ytmStepConstant / √(hdim n)) * (w.tau * w.kappa)) < (ytmStepConstant / √(hdim n)) ^ 2 * (d.dtau * d.dkappa) ∧ centerSq (addStep w d (ytmStepConstant / √(hdim n))).x (addStep w d (ytmStepConstant / √(hdim n))).tau (addStep w d (ytmStepConstant / √(hdim n))).s (addStep w d (ytmStepConstant / √(hdim n))).kappa (mu (addStep w d (ytmStepConstant / √(hdim n)))) ≤ (ytmBetaWide * mu (addStep w d (ytmStepConstant / √(hdim n)))) ^ 2

Remaining fixed-step cross-product lower bounds and centrality estimate.

This is the next isolated YTM analytic input. Compared with the previous YTM_predictor_product_and_center_estimate, this theorem no longer has to prove product positivity directly. It only has to show that each second-order product is not negative enough to cancel the first-order product term, together with the N(1/2) centrality estimate.

theorem HSDInteriorPointLP.YTM_predictor_product_and_center_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → (∀ (i : Fin n), 0 < (addStep w d (ytmStepConstant / √(hdim n))).x i * (addStep w d (ytmStepConstant / √(hdim n))).s i) ∧ 0 < (addStep w d (ytmStepConstant / √(hdim n))).tau * (addStep w d (ytmStepConstant / √(hdim n))).kappa ∧ centerSq (addStep w d (ytmStepConstant / √(hdim n))).x (addStep w d (ytmStepConstant / √(hdim n))).tau (addStep w d (ytmStepConstant / √(hdim n))).s (addStep w d (ytmStepConstant / √(hdim n))).kappa (mu (addStep w d (ytmStepConstant / √(hdim n)))) ≤ (ytmBetaWide * mu (addStep w d (ytmStepConstant / √(hdim n)))) ^ 2

Product-and-centrality part of the YTM predictor estimate, now reduced to fixed-step cross-product lower bounds plus the centrality estimate.

theorem HSDInteriorPointLP.YTM_predictor_scaled_estimate {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → Interior (addStep w d (ytmStepConstant / √(hdim n))) ∧ centerSq (addStep w d (ytmStepConstant / √(hdim n))).x (addStep w d (ytmStepConstant / √(hdim n))).tau (addStep w d (ytmStepConstant / √(hdim n))).s (addStep w d (ytmStepConstant / √(hdim n))).kappa (mu (addStep w d (ytmStepConstant / √(hdim n)))) ≤ (ytmBetaWide * mu (addStep w d (ytmStepConstant / √(hdim n)))) ^ 2

Isolated YTM predictor local estimate for the fixed step length.

This is the only remaining analytic ingredient on the predictor side. All purely algebraic bookkeeping has already been separated above: the step length is positive and at most one, the gap update is given by predictor_mu_step, and the new centrality residual is expanded by predictor_centerSq_step_eq. What remains here is the YTM scaled-direction estimate that proves both positivity preservation and the wide-neighborhood centrality bound for the fixed step ytmStepConstant / sqrt(n+1).

theorem HSDInteriorPointLP.YTM_predictor_fixed_step_local_geometry {n : ℕ} (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaTight w → HSDStepDirection w d 0 → 0 < ytmStepConstant / √(hdim n) ∧ ytmStepConstant / √(hdim n) ≤ 1 ∧ Interior (addStep w d (ytmStepConstant / √(hdim n))) ∧ HSDNeighborhood ytmBetaWide (addStep w d (ytmStepConstant / √(hdim n)))

Predictor local geometry estimate for the fixed YTM step length.

After isolating YTM_predictor_scaled_estimate, this theorem contains only the wrapping needed to turn the analytic estimate into an HSDNeighborhood statement. The complementarity-gap decrease is not part of this theorem; it is proved below from gap_addStep_of_HSDStepDirection and γ = 0.

structure HSDInteriorPointLP.YTMCorrectorEstimate (n : ℕ) : Prop

Corrector estimate used in the YTM proof.

This packages the corrector half of Theorem 6: starting from the wide neighborhood N(1/2), the corrector direction with γ = 1 accepts the full step and returns to the tight neighborhood N(1/4).

• estimate (w : HSState n) (d : HSDirection n) : HSDNeighborhood ytmBetaWide w → HSDStepDirection w d 1 → CorrectorStepGuarantee ytmBetaTight w d

theorem HSDInteriorPointLP.YTM_predictor_estimate_from_paper (n : ℕ) : YTMPredictorEstimate n

Predictor half of the YTM local neighborhood analysis.

theorem HSDInteriorPointLP.YTM_corrector_estimate_from_paper (n : ℕ) : YTMCorrectorEstimate n

Corrector half of the YTM local neighborhood analysis.

theorem HSDInteriorPointLP.YTM_fixed_local_theory_from_paper (n : ℕ) : YTMFixedLocalTheory n

Fixed-parameter YTM local-analysis obligation.

theorem HSDInteriorPointLP.predictor_step_guarantee_fixed {n : ℕ} (T : YTMFixedLocalTheory n) (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : ∃ (α : ℝ), PredictorStepGuarantee ytmBetaWide ytmStepConstant w d α

Local predictor estimate used in YTM Theorem 6, obtained from the fixed-parameter local theory.

theorem HSDInteriorPointLP.corrector_step_guarantee_fixed {n : ℕ} (T : YTMFixedLocalTheory n) (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : CorrectorStepGuarantee ytmBetaTight w d

Local corrector estimate used in YTM Theorem 6, obtained from the fixed-parameter local theory.

noncomputable def HSDInteriorPointLP.HSDNewtonDirection {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) (w : HSState n) (hw : Interior w) (γ : ℝ) : HSDirection n

Canonical Newton direction selected from the full-row-rank HLP linear algebra.

Equations

• HSDInteriorPointLP.HSDNewtonDirection P std w hw γ = HSDInteriorPointLP.chooseSearchDirection w γ ⋯

theorem HSDInteriorPointLP.HSDNewtonDirection_step {m n : ℕ} (P : LPData m n) (std : LPStandardAssumptions P) (w : HSState n) (hw : Interior w) (γ : ℝ) : HSDStepDirection w (HSDNewtonDirection P std w hw γ) γ

The selected Newton direction satisfies the reduced HSD step-direction equations.

noncomputable def HSDInteriorPointLP.ytmPredictorAlpha (n : ℕ) : ℝ

Fixed predictor step size used in the YTM estimate.

Equations

• HSDInteriorPointLP.ytmPredictorAlpha n = HSDInteriorPointLP.ytmStepConstant / √(HSDInteriorPointLP.hdim n)

theorem HSDInteriorPointLP.predictor_step_guarantee_fixed_alpha {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaTight w) (hdir : HSDStepDirection w d 0) : PredictorStepGuarantee ytmBetaWide ytmStepConstant w d (ytmPredictorAlpha n)

Predictor local guarantee at the fixed YTM step.

theorem HSDInteriorPointLP.corrector_step_guarantee_of_wide {n : ℕ} (w : HSState n) (d : HSDirection n) (hneigh : HSDNeighborhood ytmBetaWide w) (hdir : HSDStepDirection w d 1) : CorrectorStepGuarantee ytmBetaTight w d

Corrector local guarantee from the YTM wide-to-tight estimate.

noncomputable def HSDInteriorPointLP.ytmContraction (n : ℕ) : ℝ

The contraction factor appearing in the two-step YTM estimate.

Equations

• HSDInteriorPointLP.ytmContraction n = 1 - HSDInteriorPointLP.ytmStepConstant / √(HSDInteriorPointLP.hdim n)

theorem HSDInteriorPointLP.ytmContraction_nonneg (n : ℕ) : 0 ≤ ytmContraction n

The two-step contraction factor is nonnegative.

theorem HSDInteriorPointLP.ytmContraction_le_one (n : ℕ) : ytmContraction n ≤ 1

The two-step contraction factor is at most one.

theorem HSDInteriorPointLP.ytmContraction_lt_one (n : ℕ) : ytmContraction n < 1

The two-step contraction factor is strictly less than one.

theorem HSDInteriorPointLP.ytmContraction_bounds (n : ℕ) : 0 ≤ ytmContraction n ∧ ytmContraction n < 1

Collected bounds for the two-step contraction factor.

theorem HSDInteriorPointLP.ytmContraction_eq_one_sub_alpha (n : ℕ) : ytmContraction n = 1 - ytmStepConstant / √(hdim n)

The contraction factor is exactly 1 - a_n, where a_n = ytmStepConstant / sqrt(hdim n).

theorem HSDInteriorPointLP.ytm_alpha_mul_log_scale (n : ℕ) (u : ℝ) : ytmStepConstant / √(hdim n) * (√(hdim n) / ytmStepConstant * u) = u

The reciprocal scale used in the logarithmic iteration bound cancels the YTM step coefficient.

theorem HSDInteriorPointLP.one_sub_pow_le_exp_neg_mul_nat {a : ℝ} (ha_le_one : a ≤ 1) (K : ℕ) : (1 - a) ^ K ≤ Real.exp (-(a * ↑K))

Elementary exponential majorization used for the YTM contraction: if a ≤ 1, then (1-a)^K ≤ exp(-aK).

theorem HSDInteriorPointLP.YTM_contraction_power_le_exp {n : ℕ} (K : ℕ) : ytmContraction n ^ K ≤ Real.exp (-(ytmStepConstant / √(hdim n) * ↑K))

The YTM contraction power is bounded by the corresponding exponential decay.

theorem HSDInteriorPointLP.ytm_exp_mul_gap_le_of_log_bound {n : ℕ} (K : ℕ) {gap0 ε : ℝ} (hgap0 : 0 < gap0) (hε_pos : 0 < ε) (hK : √(hdim n) / ytmStepConstant * Real.log (gap0 / ε) ≤ ↑K) : Real.exp (-(ytmStepConstant / √(hdim n) * ↑K)) * gap0 ≤ ε

If the real-valued pair count satisfies the logarithmic lower bound, then the exponential estimate already puts gap0 below ε.

noncomputable def HSDInteriorPointLP.ytmLogPairBoundL (n : ℕ) (L : ℝ) : ℕ

Pair bound written using L = log(gap0 / ε).

Equations

• HSDInteriorPointLP.ytmLogPairBoundL n L = ⌈√(HSDInteriorPointLP.hdim n) / HSDInteriorPointLP.ytmStepConstant * L⌉₊

noncomputable def HSDInteriorPointLP.ytmLogIterationBoundL (n : ℕ) (L : ℝ) : ℕ

Ordinary iteration bound written using L = log(gap0 / ε).

Equations

• HSDInteriorPointLP.ytmLogIterationBoundL n L = 2 * HSDInteriorPointLP.ytmLogPairBoundL n L

def HSDInteriorPointLP.YTMGapStop {n : ℕ} (ε : ℝ) (w : HSState n) : Prop

Gap-based stopping condition used by the formalized iteration bound.

Equations

• HSDInteriorPointLP.YTMGapStop ε w = (HSDInteriorPointLP.gap w ≤ ε)

def HSDInteriorPointLP.YTMMuStop {n : ℕ} (ε : ℝ) (w : HSState n) : Prop

Duality-measure stopping condition corresponding to the paper's μ ≤ ε.

Equations

• HSDInteriorPointLP.YTMMuStop ε w = (HSDInteriorPointLP.mu w ≤ ε)

theorem HSDInteriorPointLP.YTMGapStop_of_gap_le {n : ℕ} {w : HSState n} {ε : ℝ} (hgap : gap w ≤ ε) : YTMGapStop ε w

Gap stopping immediately gives the formal gap-stop predicate.

theorem HSDInteriorPointLP.YTMMuStop_of_gap_le_hdim_mul {n : ℕ} {w : HSState n} {ε : ℝ} (hgap : gap w ≤ hdim n * ε) : YTMMuStop ε w

Since μ = gap / hdim, a scaled gap bound gives the μ ≤ ε stopping test.