OAI/Analysis/KadisonSimilarity/Representation/RadonNikodymCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Square-root Radon–Nikodym coordinates put each finite scalar spectral measure over a common finite base.

  1. def OAI.KadisonSimilarity.squareRootDensity line 17
  2. theorem OAI.KadisonSimilarity.squareRootDensity_measurable line 19
  3. theorem OAI.KadisonSimilarity.squareRootDensity_sq_ae line 22
  4. theorem OAI.KadisonSimilarity.squaredDensityMeasure_eq line 27
  5. theorem OAI.KadisonSimilarity.squareRootDensity_memLp line 36
  6. def OAI.KadisonSimilarity.radonNikodymIsometry line 49

    Source documentation

    The actual scalar L² coordinate inclusion over a dominating measure.

    def radonNikodymIsometry (hν : ν ≪ μ) : Lp ℂ 2 ν →ₗᵢ[ℂ] Lp ℂ 2 μ :=
…
  7. theorem OAI.KadisonSimilarity.radonNikodymIsometry_toLp line 53