additiveQuadratic

formal source

  11open scoped BigOperators
  12
  13/-- Quadratic additive approximation `1/2 * Σ εᵢ²`. -/
  14noncomputable def additiveQuadratic {n : ℕ} (ε : Vec n) : ℝ :=
  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 α ε