OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegralOrthogonal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Pureness.positive_mul_power_zero line 16
2. lemma OAI.Pureness.positive_sqrt_mul_zero line 26
3. abbrev OAI.Pureness.positiveSqrt line 38

   Also declared: OAI/Analysis/JiangSu/CuntzSemigroup/FiniteCuntzOrthogonal.lean:15 (same declaration text).

4. theorem OAI.Pureness.positiveSqrt_star line 40

   Also declared: OAI/Analysis/JiangSu/CuntzSemigroup/FiniteCuntzOrthogonal.lean:17 (same declaration text).

5. theorem OAI.Pureness.positiveSqrt_mul line 43

   Also declared: OAI/Analysis/JiangSu/CuntzSemigroup/FiniteCuntzOrthogonal.lean:20 (same declaration text).

6. def OAI.Pureness.finiteOrthogonalColumn line 48
7. lemma OAI.Pureness.finiteOrthogonalColumn_starMul line 53
8. lemma OAI.Pureness.finiteOrthogonalColumn_mulStar line 63
9. theorem OAI.Pureness.finiteSpectralIntegral_add_orthogonal line 75