def selfConcordantQuadraticRegion {E : Type u} (f : E → ℝ) (fStar : ℝ) (Mf : NNReal) : Set E

Definition 5.2.9: the Chapter 5 quadratic-convergence region, written in the zero-safe multiplication form 8 M_f² (f(x) - f*) ≤ 1. When M_f = 0, this is all of E, matching the degenerate quadratic regime.

def SelfConcordantQuadraticRegion.«term𝒬[_|_,_]» : Lean.ParserDescr

Source-facing notation for the Chapter 5 quadratic-convergence region Q_f.

theorem mem_selfConcordantQuadraticRegion_iff {E : Type u} {f : E → ℝ} {fStar : ℝ} {Mf : NNReal} {x : E} : x ∈ selfConcordantQuadraticRegion f fStar Mf ↔ 8 * ↑Mf ^ 2 * (f x - fStar) ≤ 1

Membership in 𝒬[f | f*, M_f] is exactly the zero-safe inequality 8 M_f² (f(x) - f*) ≤ 1.

theorem mem_selfConcordantQuadraticRegion_iff_div {E : Type u} {f : E → ℝ} {fStar : ℝ} {Mf : NNReal} (hMf : 0 < Mf) {x : E} : x ∈ selfConcordantQuadraticRegion f fStar Mf ↔ f x - fStar ≤ 1 / (8 * ↑Mf ^ 2)

In the nondegenerate regime M_f > 0, the zero-safe multiplication-form owner 𝒬[f | f*, M_f] is equivalent to the textbook divided threshold f(x) - f* ≤ 1 / (8 M_f^2).

theorem Mf_pos_of_not_mem_selfConcordantQuadraticRegion {E : Type u} {f : E → ℝ} {fStar : ℝ} {Mf : NNReal} {x : E} (hx : x ∉ selfConcordantQuadraticRegion f fStar Mf) : 0 < Mf

If x lies outside the Chapter 5 quadratic-convergence region 𝒬[f | f*, M_f], then the scaling constant M_f is necessarily positive. In the degenerate quadratic case M_f = 0, the zero-safe owner 𝒬[f | f*, M_f] is all of E.

theorem gap_pos_of_not_mem_selfConcordantQuadraticRegion {E : Type u} {f : E → ℝ} {fStar : ℝ} {Mf : NNReal} {x : E} (hx : x ∉ selfConcordantQuadraticRegion f fStar Mf) : 0 < f x - fStar

If x lies outside the Chapter 5 quadratic-convergence region 𝒬[f | f*, M_f], then its suboptimality gap f(x) - f* is positive. Nonpositive gaps automatically satisfy the zero-safe membership inequality.

theorem mem_selfConcordantQuadraticRegion_iff_mem_cubicNewtonQuadraticDecreaseRegion {E : Type u} {f : E → ℝ} {fStar σ : ℝ} {Mf L3 : NNReal} {xStar x : E} (hfStar : f xStar = fStar) (hMf : 0 < Mf) (hthreshold : 1 / (8 * ↑Mf ^ 2) = σ ^ 3 / (2 * ↑L3 ^ 2)) (hL3 : 0 < ↑L3) : x ∈ selfConcordantQuadraticRegion f fStar Mf ↔ x ∈ cubicNewtonQuadraticDecreaseRegion f xStar σ L3

If f* = f(x^*) and the Chapter 5 threshold 1 / (8 M_f^2) matches the divided Chapter 4 threshold σ^3 / (2 L₃^2) with L₃ > 0, then the Chapter 5 region Q_f agrees pointwise with the Chapter 4 quadratic-decrease region cubicNewtonQuadraticDecreaseRegion f xStar σ L3.