OAI/Analysis/KadisonKastler/L2StrataSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

L² as the Hilbert sum of measurable strata

Restriction and extension by zero identify the L² space on a countable measurable partition with the Hilbert sum of its individual L² spaces.

  1. theorem OAI.KadisonKastler.l2Extension_inner line 23
  2. theorem OAI.KadisonKastler.l2Restrict_extension_disjoint line 43
  3. theorem OAI.KadisonKastler.l2Strata_orthogonal line 60
  4. theorem OAI.KadisonKastler.l2_eq_zero_of_restrictions line 68
  5. theorem OAI.KadisonKastler.l2Strata_isHilbertSum line 84
  6. def OAI.KadisonKastler.l2StrataCoordinates line 106

    Source documentation

    The actual Hilbert-space coordinates associated with a measurable partition.

    def l2StrataCoordinates [CompleteSpace H] [Countable ι]
    (hd : Pairwise (fun i j => Disjoint (s i) (s j))) (hcover : ⋃ i, s i = Set.univ) :
    Lp H 2 μ ≃ₗᵢ[ℂ] lp (fun i => Lp H 2 (Measure.comap ((↑) : s i → X) μ)) 2 :=
…