gramSchmidt_mem_span — Mathlib

English

For each i ≤ j, the i-th GramSchmidt vector lies in the span of {f(k) : k ≤ j}.

Русский

Для каждого i ≤ j вектор GramSchmidt на позиции i лежит в линейной оболочке {f(k) : k ≤ j}.

LaTeX

$$$ gramSchmidt 𝕜 f i \in \operatorname{span}_{\mathbb{K}}(\{ \mathrm{gramSchmidt}_{\mathbb{K}} f k : k \le j \}) $$$

Lean4

theorem gramSchmidt_mem_span (f : ι → E) : ∀ {j i}, i ≤ j → gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j) :=
  by
  intro j i hij
  rw [gramSchmidt_def 𝕜 f i]
  simp_rw [starProjection_singleton]
  refine Submodule.sub_mem _ (subset_span (mem_image_of_mem _ hij)) (Submodule.sum_mem _ fun k hk => ?_)
  let hkj : k < j := (Finset.mem_Iio.1 hk).trans_le hij
  exact smul_mem _ _ (span_mono (image_mono <| Set.Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)
termination_by j => j

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