OAI/Analysis/SeparableQuotients/TreeBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.ActualSpace.TypeII.childEvals line 11
2. lemma OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly_add line 16
3. lemma OAI.SeparableQuotient.ActualSpace.TypeII.recombineEarly_mono line 22
4. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.low_refined_bound line 31
5. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.node_refined_majorant line 68
6. lemma OAI.SeparableQuotient.ActualSpace.Family.norming_crop line 82
7. lemma OAI.SeparableQuotient.ActualSpace.Family.norming_cases line 87
8. def OAI.SeparableQuotient.ActualSpace.smallBudget line 105
9. def OAI.SeparableQuotient.ActualSpace.largeUnit line 107
10. def OAI.SeparableQuotient.ActualSpace.largeBudget line 109
11. lemma OAI.SeparableQuotient.ActualSpace.smallBudget_nonneg line 112
12. lemma OAI.SeparableQuotient.ActualSpace.largeUnit_ge line 116
13. lemma OAI.SeparableQuotient.ActualSpace.largeBudget_ge line 121
14. lemma OAI.SeparableQuotient.ActualSpace.largeBudget_nonneg line 126
15. lemma OAI.SeparableQuotient.ActualSpace.smallBudget_succ line 128
16. lemma OAI.SeparableQuotient.ActualSpace.largeBudget_step line 133
17. structure OAI.SeparableQuotient.ActualSpace.DepthMajorant line 140
18. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.exists_depthMajorant line 152
19. lemma OAI.SeparableQuotient.ActualSpace.Family.qprime_formula line 224
20. lemma OAI.SeparableQuotient.ActualSpace.Family.holder_theta line 230
21. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.sum_eval_bound line 236
22. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.norm_sum_bound line 275