OAI/Analysis/BackwardIntertwiners/OrdinaryStructure.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.globalTail line 14
  2. lemma OAI.BackwardIntertwiners.mem_globalTail line 16
  3. lemma OAI.BackwardIntertwiners.globalTail_closed line 33
  4. lemma OAI.BackwardIntertwiners.constantBasis_mem_globalTail line 39
  5. lemma OAI.BackwardIntertwiners.constantBasis_not_mem_globalTail line 44
  6. lemma OAI.BackwardIntertwiners.globalTail_nonzero line 51
  7. lemma OAI.BackwardIntertwiners.globalTail_proper line 59
  8. lemma OAI.BackwardIntertwiners.globalTail_forward line 63
  9. lemma OAI.BackwardIntertwiners.globalTail_not_backward line 69
  10. def OAI.BackwardIntertwiners.sliceProjection line 83
  11. lemma OAI.BackwardIntertwiners.sliceProjection_ae line 85
  12. lemma OAI.BackwardIntertwiners.sliceProjection_singleL2 line 90
  13. lemma OAI.BackwardIntertwiners.sliceProjection_idempotent line 94
  14. lemma OAI.BackwardIntertwiners.sliceProjection_constantBasis line 97
  15. lemma OAI.BackwardIntertwiners.sliceProjection_scalar_commute line 107
  16. lemma OAI.BackwardIntertwiners.sliceProjection_zero_not_commute line 116
  17. lemma OAI.BackwardIntertwiners.sliceProjection_zero_not_scalar line 127
  18. lemma OAI.BackwardIntertwiners.residue_separates line 148
  19. def OAI.BackwardIntertwiners.residueClass line 154
  20. lemma OAI.BackwardIntertwiners.measurableSet_residueClass line 155
  21. lemma OAI.BackwardIntertwiners.residueClass_nonnull line 157
  22. def OAI.BackwardIntertwiners.residueIndicator line 169
  23. lemma OAI.BackwardIntertwiners.residueIndicator_ae line 171
  24. lemma OAI.BackwardIntertwiners.residueIndicator_ne_zero line 173
  25. lemma OAI.BackwardIntertwiners.residueIndicator_orthogonal line 182
  26. lemma OAI.BackwardIntertwiners.residueIndicator_independent line 192
  27. lemma OAI.BackwardIntertwiners.scalarHilbert_infinite line 198
  28. lemma OAI.BackwardIntertwiners.forwardOperator_singleL2_zero line 206
  29. lemma OAI.BackwardIntertwiners.coordinate_forward_single line 213
  30. lemma OAI.BackwardIntertwiners.forwardOperator_not_compact line 219
  31. lemma OAI.BackwardIntertwiners.globalHilbert_infinite line 228
  32. lemma OAI.BackwardIntertwiners.sliceProjection_selfAdjoint line 237
  33. lemma OAI.BackwardIntertwiners.sliceProjection_isStarProjection line 245