OAI/Analysis/BrownMeasure/FunctionalCalculus.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteFactor.WeightInterval line 14
  2. def OAI.FiniteFactor.sourceWeightPoint line 16
  3. lemma OAI.FiniteFactor.sourceWeightPoint_measurable line 18
  4. lemma OAI.FiniteFactor.sourceWeightPoint_val line 21
  5. def OAI.FiniteFactor.sourceContinuousWeightBase line 26
  6. def OAI.FiniteFactor.sourceContinuousWeight line 33
  7. lemma OAI.FiniteFactor.sourceContinuousWeight_apply_ae line 36
  8. lemma OAI.FiniteFactor.sourceContinuousWeight_one line 42
  9. lemma OAI.FiniteFactor.sourceContinuousWeight_zero line 49
  10. lemma OAI.FiniteFactor.sourceContinuousWeight_add line 57
  11. lemma OAI.FiniteFactor.sourceContinuousWeight_mul line 67
  12. lemma OAI.FiniteFactor.sourceContinuousWeight_smul line 77
  13. lemma OAI.FiniteFactor.sourceContinuousWeight_star line 87
  14. def OAI.FiniteFactor.sourceContinuousWeightHom line 99
  15. lemma OAI.FiniteFactor.sourceContinuousWeightHom_continuous line 109
  16. lemma OAI.FiniteFactor.sourceContinuousWeight_id line 115
  17. lemma OAI.FiniteFactor.sourceWeight_spectrum_subset line 131
  18. lemma OAI.FiniteFactor.sourceContinuousWeightHom_eq_cfc line 137
  19. lemma OAI.FiniteFactor.sourcePi_trace line 145