OAI/Analysis/WeakInfiniteness/FellAbsorption.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakPureInfiniteness.HilbertValued.HilbertSum line 18
2. lemma OAI.WeakPureInfiniteness.HilbertValued.mem_l2_reindex line 25
3. def OAI.WeakPureInfiniteness.HilbertValued.l2Reindex line 32
4. lemma OAI.WeakPureInfiniteness.HilbertValued.l2Reindex_apply line 48
5. lemma OAI.WeakPureInfiniteness.HilbertValued.l2Reindex_single line 52
6. lemma OAI.WeakPureInfiniteness.HilbertValued.l2_summable_norm_sq line 65
7. lemma OAI.WeakPureInfiniteness.HilbertValued.l2_norm_sq line 71
8. lemma OAI.WeakPureInfiniteness.HilbertValued.weighted_two_mul_le line 76
9. def OAI.WeakPureInfiniteness.HilbertValued.permutationSum line 83
10. lemma OAI.WeakPureInfiniteness.HilbertValued.weighted_squares_summable line 87
11. lemma OAI.WeakPureInfiniteness.HilbertValued.weighted_squares_sum_le line 100
12. theorem OAI.WeakPureInfiniteness.HilbertValued.norm_permutationSum_le line 115
13. def OAI.WeakPureInfiniteness.HilbertValued.l2Diagonal line 174
14. lemma OAI.WeakPureInfiniteness.HilbertValued.l2Diagonal_apply line 196
15. lemma OAI.WeakPureInfiniteness.HilbertValued.l2Diagonal_symm_apply line 202
16. def OAI.WeakPureInfiniteness.HilbertValued.fellUnitary line 207
17. def OAI.WeakPureInfiniteness.HilbertValued.twistedRegular line 210
18. lemma OAI.WeakPureInfiniteness.HilbertValued.twistedRegular_apply line 218
19. theorem OAI.WeakPureInfiniteness.HilbertValued.fell_intertwines line 221
20. theorem OAI.WeakPureInfiniteness.HilbertValued.norm_twistedRegular_sum line 232