OAI/Analysis/RotationWeights/BorelWeights.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ContinuousCircleWeight.RealBorel line 20
  2. instance OAI.ContinuousCircleWeight.(instance at line 25) line 25
  3. def OAI.ContinuousCircleWeight.RealBorel.const line 27
  4. def OAI.ContinuousCircleWeight.RealBorel.add line 28
  5. def OAI.ContinuousCircleWeight.RealBorel.mul line 31
  6. def OAI.ContinuousCircleWeight.RealBorel.shift line 34
  7. def OAI.ContinuousCircleWeight.RealBorel.ofContinuous line 36
  8. def OAI.ContinuousCircleWeight.realPi line 40
  9. def OAI.ContinuousCircleWeight.realPiField line 43
  10. lemma OAI.ContinuousCircleWeight.realPiField_apply line 45
  11. lemma OAI.ContinuousCircleWeight.realPiField_bound line 47
  12. lemma OAI.ContinuousCircleWeight.realPi_coe line 49
  13. lemma OAI.ContinuousCircleWeight.realPi_norm_le line 52
  14. lemma OAI.ContinuousCircleWeight.realPi_congr line 53
  15. lemma OAI.ContinuousCircleWeight.realPi_continuous line 56
  16. lemma OAI.ContinuousCircleWeight.realPi_add line 60
  17. lemma OAI.ContinuousCircleWeight.realPi_mul line 70
  18. lemma OAI.ContinuousCircleWeight.realPi_one line 79
  19. lemma OAI.ContinuousCircleWeight.realPi_commute line 88
  20. lemma OAI.ContinuousCircleWeight.realPiField_symmetric line 93
  21. lemma OAI.ContinuousCircleWeight.realPi_selfAdjoint line 100
  22. lemma OAI.ContinuousCircleWeight.realPi_commutes line 109
  23. lemma OAI.ContinuousCircleWeight.realPi_injective line 112
  24. lemma OAI.ContinuousCircleWeight.realPi_shift line 124
  25. def OAI.ContinuousCircleWeight.realCutoff line 143
  26. def OAI.ContinuousCircleWeight.realCutoffInv line 149
  27. lemma OAI.ContinuousCircleWeight.realCutoff_proj line 162
  28. lemma OAI.ContinuousCircleWeight.realCutoff_mul_inv line 170
  29. def OAI.ContinuousCircleWeight.realCutoffRange line 182
  30. instance OAI.ContinuousCircleWeight.realCutoffRange_complete line 184
  31. lemma OAI.ContinuousCircleWeight.realCutoffRange_projection line 186
  32. lemma OAI.ContinuousCircleWeight.realCutoffRange_le line 190
  33. lemma OAI.ContinuousCircleWeight.realPi_tendsto line 196
  34. lemma OAI.ContinuousCircleWeight.realCutoffRange_tendsto line 211