OAI/Analysis/Commutator/CyclicSpectralMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CyclicSpectral.complexify line 20
2. lemma OAI.Kadison.CyclicSpectral.complexify_add line 23
3. lemma OAI.Kadison.CyclicSpectral.complexify_smul line 27
4. lemma OAI.Kadison.CyclicSpectral.complexify_sub line 31
5. lemma OAI.Kadison.CyclicSpectral.complexify_nonneg line 35
6. def OAI.Kadison.CyclicSpectral.vectorFunctional line 39
7. def OAI.Kadison.CyclicSpectral.measure line 53
8. instance OAI.Kadison.CyclicSpectral.measure_regular line 56
9. instance OAI.Kadison.CyclicSpectral.measure_finite line 59
10. lemma OAI.Kadison.CyclicSpectral.integral_real line 62