multiplicativeQuadratic

formal source

  15  (1 / 2 : ℝ) * ∑ i : Fin n, (ε i) ^ 2
  16
  17/-- Quadratic multiplicative approximation `1/2 * (Σ αᵢ εᵢ)²`. -/
  18noncomputable def multiplicativeQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=
  19  (1 / 2 : ℝ) * (dot α ε) ^ 2
  20
  21/-- Residual compensatory quadratic term. -/
  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