OAI/Analysis/Commutator/CyclicSpectralNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CyclicSpectral.normSqFunction line 22
2. lemma OAI.Kadison.CyclicSpectral.complexify_normSq line 27
3. lemma OAI.Kadison.CyclicSpectral.representation_norm_integral line 32
4. lemma OAI.Kadison.CyclicSpectral.toLp_norm_eq line 44