range_linearIsometry — Mathlib

English

If V is an orthogonal family that forms a Hilbert sum, then the associated surjective isometry exists between E and lp G 2.

Русский

Если V образует ортогональную систему и образует Гильбертову сумму, тогда существует сюръективная изометрия между E и lp G 2.

LaTeX

$$$ IsHilbertSum.mk\\, (V) \\, : \\, E \\cong lp G 2 $$$

Lean4

/-- The canonical linear isometry from the `lp 2` of a mutually orthogonal family of subspaces of
`E` into E, has range the closure of the span of the subspaces. -/
protected theorem range_linearIsometry [∀ i, CompleteSpace (G i)] :
    LinearMap.range hV.linearIsometry.toLinearMap = (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure := by
  classical
  refine le_antisymm ?_ ?_
  · rintro x ⟨f, rfl⟩
    refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)
    intro s
    rw [SetLike.mem_coe]
    refine sum_mem ?_
    intro i _
    refine mem_iSup_of_mem i ?_
    exact LinearMap.mem_range_self _ (f i)
  · apply topologicalClosure_minimal
    · refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x
    exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed

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