OAI/Analysis/SeparableQuotients/NormingBounds.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.FiniteVectors.norm_mask_le_explicit line 12
2. lemma OAI.SeparableQuotient.FiniteVectors.norm_le_four line 18
3. lemma OAI.SeparableQuotient.FiniteVectors.single_support_bounds line 30
4. lemma OAI.SeparableQuotient.ActualSpace.Family.base_zero line 62
5. lemma OAI.SeparableQuotient.ActualSpace.Family.base_crop line 67
6. lemma OAI.SeparableQuotient.ActualSpace.Family.stage_crop line 80
7. lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_nonzero_witness line 84
8. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.base_eval_unique line 91
9. def OAI.SeparableQuotient.ActualSpace.ThinnedWindows.evalVector line 120
10. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.evalVector_nonneg line 124
11. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.evalVector_base line 128
12. def OAI.SeparableQuotient.ActualSpace.TypeII.continuation line 155
13. lemma OAI.SeparableQuotient.ActualSpace.TypeII.continuation_nonneg line 162
14. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.node_majorant line 168
15. def OAI.SeparableQuotient.ActualSpace.TypeII.boundaryVector line 193
16. def OAI.SeparableQuotient.ActualSpace.TypeII.continuationVector line 197
17. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.epsilonVector_norm line 201
18. lemma OAI.SeparableQuotient.ActualSpace.TypeII.boundaryVector_norm line 213
19. lemma OAI.SeparableQuotient.ActualSpace.TypeII.continuation_norm line 219
20. lemma OAI.SeparableQuotient.ActualSpace.TypeII.continuationVector_norm line 230
21. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.node_uniform line 238
22. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.stage_uniform line 261
23. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.norming_uniform line 283