OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegral.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Pureness.finiteDimensionDistribution line 14
  2. lemma OAI.Pureness.finiteDimensionDistribution_antitone line 18
  3. lemma OAI.Pureness.finiteDimensionDistribution_measurable line 25
  4. def OAI.Pureness.finiteSpectralIntegral line 31
  5. lemma OAI.Pureness.finiteSpectralIntegral_zero line 35
  6. theorem OAI.Pureness.finiteSpectralIntegral_inclusion line 42
  7. theorem OAI.Pureness.finiteSpectralIntegral_block_add line 48
  8. theorem OAI.Pureness.supported_cfc_polar_factor line 64
  9. theorem OAI.Pureness.positive_cut_polar_cuntz line 101
  10. lemma OAI.Pureness.finitePositiveClass_cut_polar line 114
  11. theorem OAI.Pureness.finiteSpectralIntegral_polar line 121