OAI/Analysis/KadisonSimilarity/Derivation/CyclicSpectralIsometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The cyclic spectral isometry gives scalar L² coordinates for the closed cyclic orbit, as required for central cyclic decomposition.

  1. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.inner_toLp line 17
  2. def OAI.KadisonSimilarity.VectorSpectralMeasure.vectorLinear line 33
  3. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.norm_toLp line 37
  4. def OAI.KadisonSimilarity.VectorSpectralMeasure.cyclicMap line 44
  5. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.cyclicMap_toLp line 46
  6. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.norm_cyclicMap line 51
  7. def OAI.KadisonSimilarity.VectorSpectralMeasure.cyclicIsometry line 57
  8. lemma OAI.KadisonSimilarity.VectorSpectralMeasure.cyclicMap_range line 61

    Source documentation

    The scalar spectral map identifies L² with exactly the closed cyclic orbit.

    lemma cyclicMap_range : Set.range (cyclicMap Φ v) =
    closure (Set.range (fun f : C(X, ℂ) => Φ f v)) := by
…

    Mentions: OAI.KadisonSimilarity.VectorSpectralMeasure.cyclicMap