def affineBarrierRegularizedPayoff {E : Type u} [AddCommGroup E] [Module ℝ E] (x0 : E) (β : ℝ) (ℓ : E →ᵃ[ℝ] ℝ) (F : E → ℝ) (x : E) : ℝ

The barrier-regularized affine payoff ℓ(x) - β (F(x) - F(x₀)) attached to an affine functional ℓ, a barrier term F, and a base point x₀.

theorem affineBarrierRegularizedPayoff_def {E : Type u} [AddCommGroup E] [Module ℝ E] (x0 : E) (β : ℝ) (ℓ : E →ᵃ[ℝ] ℝ) (F : E → ℝ) (x : E) : affineBarrierRegularizedPayoff x0 β ℓ F x = ℓ x - β * (F x - F x0)

Expanding affineBarrierRegularizedPayoff x₀ β ℓ F x gives the affine value ℓ(x) minus the barrier penalty β (F(x) - F(x₀)).

theorem affineBarrierRegularizedPayoff_max_le_affine_max {E : Type u} [AddCommGroup E] [Module ℝ E] {P : Set E} {F : E → ℝ} {ℓ : E →ᵃ[ℝ] ℝ} {x0 xStar xBeta : E} {β : ℝ} (hβ : 0 < β) (hx0 : x0 ∈ constrainedArgmin P F) (hxStar_mem : xStar ∈ P) (hxStar_max : IsMaxOn (⇑ℓ) P xStar) (hxBeta_mem : xBeta ∈ P) (hxBeta_max : IsMaxOn (affineBarrierRegularizedPayoff x0 β ℓ F) P xBeta) : affineBarrierRegularizedPayoff x0 β ℓ F xBeta ≤ ℓ xStar

Lemma 7.11 (1): if xBeta belongs to P and maximizes the barrier-regularized affine payoff there, xStar belongs to P and maximizes ℓ there, and x₀ minimizes F on P, then ℓ⋆(β) ≤ ℓ⋆.

theorem affine_value_sub_base_on_segment {E : Type u} [AddCommGroup E] [Module ℝ E] {ℓ : E →ᵃ[ℝ] ℝ} {x0 xStar : E} (α : ℝ) : ℓ (x0 + α • (xStar - x0)) - ℓ x0 = α * (ℓ xStar - ℓ x0)

Helper for Lemma 7.11: along the segment from x₀ to xStar, the affine increment of ℓ matches the scalar increment α (ℓ(xStar) - ℓ(x₀)).

theorem base_value_le_affineBarrierRegularizedPayoff_max {E : Type u} [AddCommGroup E] [Module ℝ E] {P : Set E} {F : E → ℝ} {ℓ : E →ᵃ[ℝ] ℝ} {x0 xBeta : E} {β : ℝ} (hx0 : x0 ∈ constrainedArgmin P F) (hxBeta_max : IsMaxOn (affineBarrierRegularizedPayoff x0 β ℓ F) P xBeta) : ℓ x0 ≤ affineBarrierRegularizedPayoff x0 β ℓ F xBeta

Helper for Lemma 7.11: the attained regularized maximum is at least the base affine value ℓ(x₀).

theorem regularized_gap_bound_along_segment {E : Type u} [AddCommGroup E] [Module ℝ E] {P : Set E} {F : E → ℝ} {ℓ : E →ᵃ[ℝ] ℝ} {x0 xStar xBeta : E} {β v : ℝ} (hβ : 0 < β) (hxStar_mem : xStar ∈ P) (hxBeta_max : IsMaxOn (affineBarrierRegularizedPayoff x0 β ℓ F) P xBeta) (hsegment_mem : ∀ ⦃x : E⦄, x ∈ P → ∀ ⦃α : ℝ⦄, α ∈ Set.Ico 0 1 → x0 + α • (x - x0) ∈ P) (hF_segment : ∀ ⦃x : E⦄, x ∈ P → ∀ ⦃α : ℝ⦄, α ∈ Set.Ico 0 1 → F (x0 + α • (x - x0)) ≤ F x0 - v * Real.log (1 - α)) {α : ℝ} (hα : α ∈ Set.Ico 0 1) : α * (ℓ xStar - ℓ x0) + β * v * Real.log (1 - α) ≤ affineBarrierRegularizedPayoff x0 β ℓ F xBeta - ℓ x0

Helper for Lemma 7.11: every admissible segment point from x₀ to xStar yields the common regularized-gap inequality used in both quantitative estimates.

theorem affineMax_le_affineBarrierRegularizedPayoff_max_add_logTerm {E : Type u} [AddCommGroup E] [Module ℝ E] {P : Set E} {F : E → ℝ} {ℓ : E →ᵃ[ℝ] ℝ} {x0 xStar xBeta : E} {β v : ℝ} (hβ : 0 < β) (hv : 0 < v) (hx0 : x0 ∈ constrainedArgmin P F) (hxStar_mem : xStar ∈ P) (hxStar_max : IsMaxOn (⇑ℓ) P xStar) (hxBeta_mem : xBeta ∈ P) (hxBeta_max : IsMaxOn (affineBarrierRegularizedPayoff x0 β ℓ F) P xBeta) (hsegment_mem : ∀ ⦃x : E⦄, x ∈ P → ∀ ⦃α : ℝ⦄, α ∈ Set.Ico 0 1 → x0 + α • (x - x0) ∈ P) (hF_segment : ∀ ⦃x : E⦄, x ∈ P → ∀ ⦃α : ℝ⦄, α ∈ Set.Ico 0 1 → F (x0 + α • (x - x0)) ≤ F x0 - v * Real.log (1 - α)) : ℓ xStar ≤ affineBarrierRegularizedPayoff x0 β ℓ F xBeta + β * v * (1 + max (Real.log ((ℓ xStar - ℓ x0) / (β * v))) 0)

Lemma 7.11 (2): under the same attained-maximizer setup, if every segment from x₀ to a point of P stays in P and satisfies the displayed barrier estimate, then ℓ⋆ ≤ ℓ⋆(β) + β v (1 + [log ((ℓ⋆ - ℓ₀) / (β v))]_+).

theorem neg_log_one_sub_le_div_of_mem_Ico {α : ℝ} (hα : α ∈ Set.Ico 0 1) : -Real.log (1 - α) ≤ α / (1 - α)

Helper for Lemma 7.11: on the interval 0 ≤ α < 1, the singular logarithmic term is bounded by the rational term α / (1 - α).

theorem affineMax_sub_base_le_sq_sqrt_add_sqrt_of_affineBarrierRegularizedPayoff_max {E : Type u} [AddCommGroup E] [Module ℝ E] {P : Set E} {F : E → ℝ} {ℓ : E →ᵃ[ℝ] ℝ} {x0 xStar xBeta : E} {β v : ℝ} (hβ : 0 < β) (hv : 0 < v) (hx0 : x0 ∈ constrainedArgmin P F) (hxStar_mem : xStar ∈ P) (hxStar_max : IsMaxOn (⇑ℓ) P xStar) (hxBeta_mem : xBeta ∈ P) (hxBeta_max : IsMaxOn (affineBarrierRegularizedPayoff x0 β ℓ F) P xBeta) (hsegment_mem : ∀ ⦃x : E⦄, x ∈ P → ∀ ⦃α : ℝ⦄, α ∈ Set.Ico 0 1 → x0 + α • (x - x0) ∈ P) (hF_segment : ∀ ⦃x : E⦄, x ∈ P → ∀ ⦃α : ℝ⦄, α ∈ Set.Ico 0 1 → F (x0 + α • (x - x0)) ≤ F x0 - v * Real.log (1 - α)) : ℓ xStar - ℓ x0 ≤ (√(affineBarrierRegularizedPayoff x0 β ℓ F xBeta - ℓ x0) + √(β * v)) ^ 2

Lemma 7.11 (3): under the same attained-maximizer and barrier-segment hypotheses, the affine gap from x₀ to the maximizer xStar is bounded by (sqrt (ℓ⋆(β) - ℓ₀) + sqrt (β v))².