def IsVariationalInequalitySolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (wstar : E) : Prop

Definition 1.4.3.1. Let E be a finite-dimensional normed space with norm ‖·‖_1 and dual norm ‖·‖_{1,*} on E*. Let Q ⊆ E be bounded, closed, and convex. Let B : E → E* be affine with B w = ℬ w + b, where ℬ : E → E* is linear and b ∈ E*, and assume the monotonicity condition ⟪ℬ h, h⟫_1 ≥ 0 for all h. The associated variational inequality problem (4.18) is to find w* ∈ Q such that ⟪B w*, w - w*⟫_1 ≥ 0 for all w ∈ Q.

Equations

• IsVariationalInequalitySolution Q ℬ b wstar = (wstar ∈ Q ∧ ∀ w ∈ Q, 0 ≤ ((fun (w : E) => ℬ w + b) wstar) (w - wstar))

noncomputable def variationalInequalityGap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Set E) (B : E → Module.Dual ℝ E) (w : E) : ℝ

Definition 1.4.3.2. Define the gap function ψ(w) := max_{v ∈ Q} ⟪B(v), w - v⟫_1. Consider the convex optimization problem min_{w ∈ Q} ψ(w) (equation (4.19)).

Equations

• variationalInequalityGap Q B w = sSup ((fun (v : E) => (B v) (w - v)) '' Q)

noncomputable def variationalInequalityGapOptimalValue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Set E) (B : E → Module.Dual ℝ E) : ℝ

Definition 1.4.3.2. The optimal value of the gap minimization problem min_{w ∈ Q} ψ(w).

Equations

• variationalInequalityGapOptimalValue Q B = sInf ((fun (w : E) => variationalInequalityGap Q B w) '' Q)

theorem variationalInequality.B_apply_sub_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (v w : E) : have B := fun (z : E) => ℬ z + b; (B v - B w) (v - w) = (ℬ (v - w)) (v - w)

Expanding the affine operator B w = ℬ w + b against a displacement.

theorem variationalInequality.VI_implies_pointwise_gap_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (hmono : ∀ (h : E), 0 ≤ (ℬ h) h) {wstar : E} : have B := fun (w : E) => ℬ w + b; IsVariationalInequalitySolution Q ℬ b wstar → ∀ v ∈ Q, (B v) (wstar - v) ≤ 0

Monotonicity of ℬ yields pointwise nonpositivity of the gap at a VI solution.

theorem variationalInequality.VI_implies_gap_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (hmono : ∀ (h : E), 0 ≤ (ℬ h) h) {wstar : E} : have B := fun (w : E) => ℬ w + b; IsVariationalInequalitySolution Q ℬ b wstar → variationalInequalityGap Q B wstar = 0

The gap at a VI solution is zero.

theorem variationalInequality.gap_nonneg_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Set E) (B : E → Module.Dual ℝ E) {w : E} (hw : w ∈ Q) (hbd : BddAbove ((fun (v : E) => (B v) (w - v)) '' Q)) : 0 ≤ variationalInequalityGap Q B w

Nonnegativity of the gap at points of Q, assuming boundedness of the image.

theorem variationalInequality.gap_eq_zero_implies_isMinOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Set E) (B : E → Module.Dual ℝ E) {wstar : E} (hbd : ∀ w ∈ Q, BddAbove ((fun (v : E) => (B v) (w - v)) '' Q)) (_hw : wstar ∈ Q) (hgap : variationalInequalityGap Q B wstar = 0) : IsMinOn (variationalInequalityGap Q B) Q wstar

If the gap is zero at w*, then w* minimizes the gap on Q.

theorem variationalInequality.exists_alpha_neg_quadratic {a b : ℝ} (ha : a < 0) (hb : 0 ≤ b) : ∃ (α : ℝ), 0 < α ∧ α ≤ 1 ∧ a * α + b * α ^ 2 < 0

A quadratic inequality with a negative linear coefficient can be made negative on (0,1].

theorem variationalInequality.gap_eq_zero_implies_VI {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (hmono : ∀ (h : E), 0 ≤ (ℬ h) h) (hconv : Convex ℝ Q) (hbd : ∀ w ∈ Q, BddAbove ((fun (v : E) => (ℬ v + b) (w - v)) '' Q)) {wstar : E} (hw : wstar ∈ Q) (hgap : variationalInequalityGap Q (fun (w : E) => ℬ w + b) wstar = 0) : IsVariationalInequalitySolution Q ℬ b wstar

Zero gap forces the variational inequality, using convexity and monotonicity.

theorem variationalInequality.isMinOn_gap_eq_zero_of_exists_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : Set E) (B : E → Module.Dual ℝ E) {wstar : E} (hbd : ∀ w ∈ Q, BddAbove ((fun (v : E) => (B v) (w - v)) '' Q)) (hw : wstar ∈ Q) : IsMinOn (variationalInequalityGap Q B) Q wstar → (∃ w0 ∈ Q, variationalInequalityGap Q B w0 = 0) → variationalInequalityGap Q B wstar = 0

A gap minimizer has zero gap when a zero-gap point exists in Q.

theorem variationalInequality_solution_iff_gap_minimizer {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (wstar : E) (hmono : ∀ (h : E), 0 ≤ (ℬ h) h) (hconv : Convex ℝ Q) (hbd : ∀ w ∈ Q, BddAbove ((fun (v : E) => (ℬ v + b) (w - v)) '' Q)) (hex : ∃ (w0 : E), IsVariationalInequalitySolution Q ℬ b w0) : have B := fun (w : E) => ℬ w + b; (IsVariationalInequalitySolution Q ℬ b wstar ↔ wstar ∈ Q ∧ IsMinOn (variationalInequalityGap Q B) Q wstar) ∧ (IsVariationalInequalitySolution Q ℬ b wstar → variationalInequalityGap Q B wstar = 0)

Lemma 1.4.3.1. A point w* solves the gap minimization problem min_{w ∈ Q} ψ(w) (4.19) if and only if it solves the variational inequality (4.18). Moreover, for every solution w* of (4.18) we have ψ(w*) = 0.

theorem variationalInequality_gap_smoothedOracle_pointwise_rearrange {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ℬ : E →L[ℝ] E →L[ℝ] ℝ) (b : Module.Dual ℝ E) (d : E → ℝ) (μ : ℝ) (x u : E) : (ℬ x) u - (b u - (ℬ u) u) - μ * d u = (ℬ x) u - μ * d u - b u + (ℬ u) u

Rearrangement of the smoothed max integrand used in Proposition 1.4.3.1.

theorem variationalInequality_gap_smoothedOracle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →L[ℝ] E →L[ℝ] ℝ) (b : Module.Dual ℝ E) (d : E → ℝ) (μ : ℝ) : have _fhat := fun (x : E) => b x; have phihat := fun (u : E) => b u - (ℬ u) u; have fμ := SmoothedMaxFunction Q ℬ phihat d μ; ∀ (x : E), fμ x = sSup ((fun (u : E) => (ℬ x) u - μ * d u - b u + (ℬ u) u) '' Q)

Proposition 1.4.3.1. A primal max-structure representation of the objective ψ in (4.19) is obtained by taking E1 = E2 = E, Q1 = Q2 = Q, d1 = d2 = d, A = ℬ, fhat(x) = ⟪b,x⟫_1, and phihat(u) = ⟪b,u⟫_1 + ⟪ℬ u,u⟫_1. Then the smoothed oracle computation for f_μ(x) reduces to solving max_{u ∈ Q} {⟪ℬ x,u⟫_1 - μ d(u) - ⟪b,u⟫_1 + ⟪ℬ u,u⟫_1} (equation (4.20)).

theorem variationalInequality_iteration_complexity_const_nonneg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) {σ1 D1 ε : ℝ} (hε : 0 < ε) (hσ1 : 0 < σ1) (hD1 : 0 ≤ D1) : 0 ≤ 4 * D1 * OperatorNormDef ℬ / (σ1 * ε)

The iteration-complexity constant in Proposition 1.4.3.2 is nonnegative.

theorem exists_nat_floor_sandwich {C : ℝ} (hC : 0 ≤ C) : ∃ (N : ℕ), ↑N ≤ C ∧ C < ↑N + 1

Rounding a nonnegative real by the natural floor yields a nearby integer.

theorem variationalInequality_iteration_complexity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Q : Set E) (ℬ : E →ₗ[ℝ] Module.Dual ℝ E) (b : Module.Dual ℝ E) (d1 : E → ℝ) (σ1 D1 ε : ℝ) : 0 < ε → 0 < σ1 → StrongConvexOn Q σ1 d1 → IsProxDiameterBound Q d1 D1 → 0 ≤ D1 → ∃ (N : ℕ), ↑N ≤ 4 * D1 * OperatorNormDef ℬ / (σ1 * ε) ∧ 4 * D1 * OperatorNormDef ℬ / (σ1 * ε) < ↑N + 1

Proposition 1.4.3.2. Assume fhat(x) = ⟪b, x⟫_1 in Proposition 1.4.3.1 so M = 0. Then Theorem 1.4.1 yields the iteration-complexity estimate for solving the variational inequality (4.18) to accuracy ε > 0: N ≤ (4 * D1 * ‖ℬ‖_{1,2}) / (σ1 * ε) (equation (4.21)).