theorem Section04Part7.matrixGame_entropy_opNorm_bound (n m : ℕ) (A : (PiLp 1 fun (x : Fin n) => ℝ) →L[ℝ] (PiLp 1 fun (x : Fin m) => ℝ) →L[ℝ] ℝ) (f : (PiLp 1 fun (x : Fin n) => ℝ) → ℝ) (φ : (PiLp 1 fun (x : Fin m) => ℝ) → ℝ) (xhat : PiLp 1 fun (x : Fin n) => ℝ) (uhat : PiLp 1 fun (x : Fin m) => ℝ) (N : ℕ) : have A' := { toFun := fun (x : PiLp 1 fun (x : Fin n) => ℝ) => ↑(A x), map_add' := ⋯, map_smul' := ⋯ }; have AEntry := fun (i : Fin n) (j : Fin m) => (A' ((PiLp.basisFun 1 ℝ (Fin n)) i)) ((PiLp.basisFun 1 ℝ (Fin m)) j); have maxEntry := sSup {r : ℝ | ∃ (i : Fin n) (j : Fin m), r = |AEntry i j|}; OperatorNormDef A' = sSup {r : ℝ | ∃ (x : PiLp 1 fun (x : Fin n) => ℝ), ‖x‖ = 1 ∧ r = DualNormDef (A' x)} ∧ OperatorNormDef A' = maxEntry ∧ (0 ≤ f xhat - φ uhat ∧ f xhat - φ uhat ≤ 4 * √(Real.log ↑n * Real.log ↑m) / (↑N + 1) * OperatorNormDef A' → 0 ≤ f xhat - φ uhat ∧ f xhat - φ uhat ≤ 4 * √(Real.log ↑n * Real.log ↑m) / (↑N + 1) * maxEntry)

Proposition 1.4.1.2. Under the entropy-distance setup of Lemma 1.4.1.1, the operator norm satisfies ‖A‖_{1,2} = max_{‖x‖_1=1} ‖A x‖_{2,*} = max_{i,j} |A^{(i,j)}| (eq:opnorm_entropy). Consequently, since M = 0 for the linear term fhat(x) = ⟪c,x⟫_1, the estimate (4.3) of Theorem 1.4.1 becomes 0 ≤ f(ĥx) - φ(ĥu) ≤ (4 * sqrt(ln n ln m)/(N+1)) * max_{i,j} |A^{(i,j)}| (4.12).

theorem Section04Part7.matrixGame.standardSimplex_coord_le_one {n : ℕ} {x : Fin n → ℝ} (hx : x ∈ standardSimplex n) (i : Fin n) : x i ≤ 1

A coordinate of a point in the standard simplex is at most 1.

theorem Section04Part7.matrixGame.quadratic_prox_sumSq_identity (n : ℕ) (x : Fin n → ℝ) (hx : x ∈ standardSimplex n) : ∑ i : Fin n, (x i - 1 / ↑n) ^ 2 = ∑ i : Fin n, x i ^ 2 - 1 / ↑n

A standard algebraic identity that simplifies the quadratic prox on the simplex.

theorem Section04Part7.matrixGame.norm_sq_le_sum_sq (n : ℕ) (z : Fin n → ℝ) : ‖z‖ ^ 2 ≤ ∑ i : Fin n, z i ^ 2

The squared sup norm on Fin n → ℝ is bounded by the sum of squared coordinates.

theorem Section04Part7.matrixGame.quadratic_prox_diameter_bound (n : ℕ) : IsProxDiameterBound (standardSimplex n) (fun (x : Fin n → ℝ) => 1 / 2 * ∑ i : Fin n, (x i - 1 / ↑n) ^ 2) (1 - 1 / ↑n)

The quadratic prox-function has prox-diameter bounded by 1 - 1/n on the standard simplex.

theorem Section04Part7.matrixGame.quadratic_prox_strongConvexOn (n : ℕ) : StrongConvexOn (standardSimplex n) 1 fun (x : Fin n → ℝ) => 1 / 2 * ∑ i : Fin n, (x i - 1 / ↑n) ^ 2

The quadratic prox-function is 1-strongly convex on the standard simplex.

theorem Section04Part7.matrixGame.dualNormDef_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Module.Dual ℝ E) : 0 ≤ DualNormDef s

DualNormDef is nonnegative.

theorem Section04Part7.matrixGame.operatorNormDef_eq_sSup_dualNormDef (n m : ℕ) (A : (Fin n → ℝ) →L[ℝ] (Fin m → ℝ) →L[ℝ] ℝ) : have A' := { toFun := fun (x : Fin n → ℝ) => ↑(A x), map_add' := ⋯, map_smul' := ⋯ }; OperatorNormDef A' = sSup {r : ℝ | ∃ (x : Fin n → ℝ), ‖x‖ = 1 ∧ r = DualNormDef (A' x)}

For the linear map A' induced from A, OperatorNormDef is the supremum of DualNormDef over unit vectors.

theorem Section04Part7.matrixGame.D_nonneg (k : ℕ) (hk : k ≠ 0) : 0 ≤ 1 - 1 / ↑k

For a positive natural k, the value 1 - 1/k is nonnegative.

theorem Section04Part7.matrixGame.sqrt_mul_le_one_of_le_one {a b : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hb0 : 0 ≤ b) (hb1 : b ≤ 1) : √(a * b) ≤ 1

If a, b ∈ [0, 1], then Real.sqrt (a * b) ≤ 1.

theorem Section04Part7.matrixGame.duality_gap_simplify_from_thm141_M0 {gap op lambdaMax D1 D2 : ℝ} (N : ℕ) (hop : op = √lambdaMax) (hop_nonneg : 0 ≤ op) (hD1_0 : 0 ≤ D1) (hD1_1 : D1 ≤ 1) (hD2_0 : 0 ≤ D2) (hD2_1 : D2 ≤ 1) (hgap : gap ≤ 4 * op / (↑N + 1) * √(D1 * D2)) : gap ≤ 4 * √lambdaMax / (↑N + 1)

Simplify a Theorem 1.4.1-style duality-gap bound in the Euclidean simplex setup (M = 0).