apply_sq_lt_iff_linearIndependent_of_symm

English

Under assumptions of positive definiteness, strict CS inequality is equivalent to linear independence.

Русский

При предположениях положительной определённости строгое неравенство Коши–Шварца эквивалентно линейной независимости.

LaTeX

$$(B x y)^2 < (B x x)(B y y) ↔ LinearIndependent R ![x, y]$$

Lean4

/-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite symmetric
forms. -/
theorem apply_sq_lt_iff_linearIndependent_of_symm [NoZeroSMulDivisors R M] (hp : ∀ x, x ≠ 0 → 0 < B x x) (hB : B.IsSymm)
    (x y : M) : (B x y) ^ 2 < (B x x) * (B y y) ↔ LinearIndependent R ![x, y] :=
  by
  rw [show (B x y) ^ 2 = (B x y) * (B y x) by rw [sq, ← hB.eq, RingHom.id_apply]]
  exact apply_mul_apply_lt_iff_linearIndependent B hp x y

Похожие утверждения