OAI/Analysis/KadisonSimilarity/Representation/L2HilbertSum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert sum of scalar L² spaces over one measure is the L² space of the coordinate Hilbert space. The construction uses actual L² maps.

  1. def OAI.KadisonSimilarity.l2MapIsometry line 19

    Source documentation

    Lift a Hilbert isometry pointwise to L².

    def l2MapIsometry (J : E →ₗᵢ[ℂ] F) : Lp E 2 μ →ₗᵢ[ℂ] Lp F 2 μ where
…
  2. theorem OAI.KadisonSimilarity.l2MapIsometry_ae line 31
  3. abbrev OAI.KadisonSimilarity.ScalarHilbertCoordinates line 37
  4. def OAI.KadisonSimilarity.scalarCoordinateIsometry line 39
  5. def OAI.KadisonSimilarity.l2CoordinateIsometry line 45
  6. def OAI.KadisonSimilarity.l2CoordinateProjection line 48
  7. theorem OAI.KadisonSimilarity.l2CoordinateProjection_ae line 52
  8. theorem OAI.KadisonSimilarity.l2Coordinate_inner line 56
  9. theorem OAI.KadisonSimilarity.l2Coordinate_orthogonal line 67
  10. theorem OAI.KadisonSimilarity.l2Coordinate_isHilbertSum line 88
  11. def OAI.KadisonSimilarity.l2HilbertSumEquiv line 116