additive_decomposition

formal source

  22noncomputable def compensatoryQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=
  23  additiveQuadratic ε - multiplicativeQuadratic α ε
  24
  25theorem additive_decomposition {n : ℕ} (α ε : Vec n) :
  26    additiveQuadratic ε
  27      = multiplicativeQuadratic α ε + compensatoryQuadratic α ε := by
  28  unfold compensatoryQuadratic
  29  ring
  30
  31/-- Squared Cauchy-Schwarz bound in our notation. -/
  32theorem dot_sq_le_sqNorm_mul {n : ℕ} (α ε : Vec n) :
  33    (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) := by
  34  unfold dot
  35  simpa [pow_two] using
  36    (Finset.sum_mul_sq_le_sq_mul_sq (s := (Finset.univ : Finset (Fin n))) α ε)
  37
  38/-- If `‖α‖² ≤ 1`, multiplicative quadratic cost is bounded by additive quadratic cost. -/
  39theorem multiplicative_le_additive_of_sqNorm_le_one {n : ℕ}
  40    (α ε : Vec n) (hα : dot α α ≤ 1) :
  41    multiplicativeQuadratic α ε ≤ additiveQuadratic ε := by
  42  have hsq : (dot α ε) ^ 2 ≤ ∑ i : Fin n, (ε i) ^ 2 := by
  43    have hcs : (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) :=
  44      dot_sq_le_sqNorm_mul α ε
  45    have hsum_nonneg : 0 ≤ ∑ i : Fin n, (ε i) ^ 2 := by
  46      exact Finset.sum_nonneg (fun i _ => sq_nonneg (ε i))
  47    have hmul : (dot α α) * (∑ i : Fin n, (ε i) ^ 2) ≤ 1 * (∑ i : Fin n, (ε i) ^ 2) :=
  48      mul_le_mul_of_nonneg_right hα hsum_nonneg
  49    exact le_trans hcs (by simpa using hmul)
  50  have hhalf : (0 : ℝ) ≤ 1 / 2 := by norm_num
  51  have hscaled := mul_le_mul_of_nonneg_left hsq hhalf
  52  simpa [multiplicativeQuadratic, additiveQuadratic, one_mul] using hscaled
  53
  54/-- Under normalized weights (`‖α‖² ≤ 1`), the compensatory term is nonnegative. -/
  55theorem compensatory_nonneg_of_sqNorm_le_one {n : ℕ}