OAI/Analysis/BackwardIntertwiners/DiagonalSymbols.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.diagonalSymbols line 16
  2. abbrev OAI.BackwardIntertwiners.DiagonalSymbol line 36
  3. instance OAI.BackwardIntertwiners.DiagonalSymbol.(instance at line 38) line 38
  4. lemma OAI.BackwardIntertwiners.DiagonalSymbol.measurable line 39
  5. def OAI.BackwardIntertwiners.DiagonalSymbol.bound line 40
  6. lemma OAI.BackwardIntertwiners.DiagonalSymbol.bound_nonneg line 41
  7. lemma OAI.BackwardIntertwiners.DiagonalSymbol.norm_le_bound line 42
  8. lemma OAI.BackwardIntertwiners.DiagonalSymbol.zero_apply line 44
  9. lemma OAI.BackwardIntertwiners.DiagonalSymbol.one_apply line 45
  10. lemma OAI.BackwardIntertwiners.DiagonalSymbol.add_apply line 46
  11. lemma OAI.BackwardIntertwiners.DiagonalSymbol.mul_apply line 47
  12. lemma OAI.BackwardIntertwiners.DiagonalSymbol.sub_apply line 48
  13. lemma OAI.BackwardIntertwiners.DiagonalSymbol.star_apply line 49
  14. lemma OAI.BackwardIntertwiners.DiagonalSymbol.smul_apply line 50
  15. lemma OAI.BackwardIntertwiners.DiagonalSymbol.algebraMap_apply line 51
  16. lemma OAI.BackwardIntertwiners.DiagonalSymbol.pow_apply line 53
  17. def OAI.BackwardIntertwiners.diagonalFiber line 57
  18. lemma OAI.BackwardIntertwiners.diagonalFiber_apply line 59
  19. lemma OAI.BackwardIntertwiners.diagonalFiber_norm line 61
  20. lemma OAI.BackwardIntertwiners.diagonalFiber_measurable line 63
  21. def OAI.BackwardIntertwiners.diagonalOperator line 69
  22. lemma OAI.BackwardIntertwiners.diagonalOperator_ae line 72
  23. lemma OAI.BackwardIntertwiners.diagonalOperator_coord line 75
  24. lemma OAI.BackwardIntertwiners.diagonalOperator_norm_le line 79
  25. lemma OAI.BackwardIntertwiners.diagonalOperator_zero line 94
  26. lemma OAI.BackwardIntertwiners.diagonalOperator_one line 101
  27. lemma OAI.BackwardIntertwiners.diagonalOperator_add line 107
  28. lemma OAI.BackwardIntertwiners.diagonalOperator_mul line 116
  29. lemma OAI.BackwardIntertwiners.diagonalOperator_smul line 125
  30. lemma OAI.BackwardIntertwiners.diagonalFiber_inner line 134
  31. lemma OAI.BackwardIntertwiners.diagonalOperator_star line 141
  32. def OAI.BackwardIntertwiners.diagonalRepresentation line 153
  33. def OAI.BackwardIntertwiners.fullMultiplierAlgebra line 168