pith. machine review for the scientific record. sign in
theorem proved term proof

dot_sq_le_sqNorm_mul

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  32theorem dot_sq_le_sqNorm_mul {n : ℕ} (α ε : Vec n) :
  33    (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) := by

proof body

Term-mode proof.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.