OAI/Analysis/BackwardIntertwiners/StrongClosure.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BackwardIntertwiners.L2_norm_eq_sqrt line 15
  2. lemma OAI.BackwardIntertwiners.L2_tendsto_zero_of_dominated line 23
  3. lemma OAI.BackwardIntertwiners.fiber_norm_sq line 40
  4. lemma OAI.BackwardIntertwiners.fiber_tendsto_zero_of_dominated line 42
  5. lemma OAI.BackwardIntertwiners.diagonalFiber_bound line 57
  6. lemma OAI.BackwardIntertwiners.diagonalFiber_tendsto_zero line 69
  7. lemma OAI.BackwardIntertwiners.L2_integrable_bound_sq line 82
  8. lemma OAI.BackwardIntertwiners.diagonalOperator_tendsto_zero line 87
  9. lemma OAI.BackwardIntertwiners.diagonalOperator_tendsto line 100
  10. def OAI.BackwardIntertwiners.strongOperatorTopology line 121
  11. def OAI.BackwardIntertwiners.StronglyClosed line 124
  12. lemma OAI.BackwardIntertwiners.strong_continuous_apply line 128
  13. lemma OAI.BackwardIntertwiners.StronglyClosed.mem_of_tendsto line 133
  14. def OAI.BackwardIntertwiners.strongGenerated line 145
  15. lemma OAI.BackwardIntertwiners.mem_strongGenerated line 147
  16. lemma OAI.BackwardIntertwiners.subset_strongGenerated line 151
  17. lemma OAI.BackwardIntertwiners.strongGenerated_le line 154
  18. lemma OAI.BackwardIntertwiners.strongGenerated_closed line 157
  19. lemma OAI.BackwardIntertwiners.strongGenerated_mono line 165
  20. lemma OAI.BackwardIntertwiners.strong_centralizer_closed line 169
  21. lemma OAI.BackwardIntertwiners.strongGenerated_commutative line 184