exists_ge_zero_eq_rootForm — Mathlib

English

There exists a nonnegative element in S whose algebra image equals RootForm(x,x) for some x in the span.

Русский

Существует неотрицанный элемент в S, чье алгебраическое отображение равно RootForm(x,x) для некоторого x в охват.

LaTeX

$$$\\exists s \\ge 0, \\ algebraMap\\ S R\\ s = P.RootForm x x$$$

Lean4

theorem exists_ge_zero_eq_rootForm (x : M) (hx : x ∈ span S (range P.root)) :
    ∃ s ≥ 0, algebraMap S R s = P.RootForm x x :=
  by
  refine ⟨(P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩, IsSumSq.nonneg ?_, by simp [posRootForm]⟩
  choose s hs using P.coroot'_apply_apply_mem_of_mem_span S hx
  suffices (P.posRootForm S).posForm ⟨x, hx⟩ ⟨x, hx⟩ = ∑ i, s i * s i from this ▸ IsSumSq.sum_mul_self Finset.univ s
  apply FaithfulSMul.algebraMap_injective S R
  simp only [posRootForm, RootPositiveForm.algebraMap_posForm, map_sum, map_mul]
  simp [hs, rootForm_apply_apply]

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