OAI/Topology/CoarseAssembly/CountableHilbertSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Separable countable sums of the Hilbert spaces in analytic cycles

  1. abbrev OAI.CoarseAssembly.Analytic.HilbertSum line 16
  2. instance OAI.CoarseAssembly.Analytic.hilbertSum_secondCountable line 18
  3. abbrev OAI.CoarseAssembly.Analytic.countableHilbertSpace line 39
  4. def OAI.CoarseAssembly.Analytic.summandIsometry line 47

    Source documentation

    The inclusion of an individual Hilbert summand.

    def summandIsometry (j : ℕ) : H j →ₗᵢ[ℂ] countableHilbertSpace H where
…

    Mentions: OAI.CoarseAssembly.Analytic.countableHilbertSpace

  5. theorem OAI.CoarseAssembly.Analytic.summandIsometry_apply line 55
  6. theorem OAI.CoarseAssembly.Analytic.summandIsometry_adjoint line 59

    Source documentation

    Coordinate evaluation is the adjoint of summand inclusion.

    theorem summandIsometry_adjoint (j : ℕ) :
    (summandIsometry H j).toContinuousLinearMap.adjoint = lp.evalCLM ℂ (fun j => H j) 2 j := by
…

    Mentions: OAI.CoarseAssembly.Analytic.summandIsometry