OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegralCommuting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Pureness.finiteSpectralIntegral_add_commute line 17
2. theorem OAI.Pureness.positive_cut_smul line 82
3. lemma OAI.Pureness.finitePositiveClass_smul line 98
4. lemma OAI.Pureness.finiteDimensionDistribution_smul line 105
5. lemma OAI.Pureness.positive_halfline_integral_div line 120
6. theorem OAI.Pureness.finiteSpectralIntegral_smul line 136