English
Restriction of a symmetric form to a complementary subspace is nondegenerate.
Русский
Ограничение симметричной формы к комплементарному подпространству невырождено.
LaTeX
$$nondegenerate_restrict_of_isCompl_ker$$
Lean4
/-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite forms. -/
theorem apply_mul_apply_lt_iff_linearIndependent [NoZeroSMulDivisors R M] (hp : ∀ x, x ≠ 0 → 0 < B x x) (x y : M) :
(B x y) * (B y x) < (B x x) * (B y y) ↔ LinearIndependent R ![x, y] :=
by
have hle : ∀ z, 0 ≤ B z z := by
intro z
by_cases hz : z = 0; simp [hz]
exact le_of_lt (hp z hz)
constructor
· contrapose!
intro h
rw [LinearIndependent.pair_iff] at h
push_neg at h
obtain ⟨r, s, hl, h0⟩ := h
by_cases hr : r = 0; · simp_all
by_cases hs : s = 0; · simp_all
suffices (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x))
by
simp only [map_smul, smul_apply, smul_eq_mul] at this
rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by ring,
show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x) by ring] at this
have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
exact le_of_eq <| mul_right_injective₀ hrs this
simp [show s • y = -r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]
· contrapose!
intro h
refine
not_linearIndependent_of_apply_mul_apply_eq B hp x y
(le_antisymm (apply_mul_apply_le_of_forall_zero_le B hle x y) h)
