OAI/Analysis/Commutator/CornerCenteredEstimates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FinitePatching.cornerScalar line 22
2. def OAI.Kadison.FinitePatching.cornerCenter line 24
3. lemma OAI.Kadison.FinitePatching.projection_trace_real line 26
4. lemma OAI.Kadison.FinitePatching.projection_trace_norm line 32
5. lemma OAI.Kadison.FinitePatching.cornerCenter_left line 39
6. lemma OAI.Kadison.FinitePatching.cornerCenter_right line 44
7. lemma OAI.Kadison.FinitePatching.cornerCenter_trace line 50
8. lemma OAI.Kadison.FinitePatching.compress_center line 57
9. lemma OAI.Kadison.FinitePatching.compressed_bound line 69
10. lemma OAI.Kadison.FinitePatching.trace_centered_compression_bound line 93
11. lemma OAI.Kadison.FinitePatching.trace_single_support_bound line 104
12. lemma OAI.Kadison.FinitePatching.cornerScalar_complement_bound line 113