OAI/Analysis/SeparableQuotients/TreeCharges.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SeparableQuotient.ActualSpace.TypeI.eval_crop_sum line 11
2. def OAI.SeparableQuotient.ActualSpace.TypeI.lowAssign line 17
3. lemma OAI.SeparableQuotient.ActualSpace.TypeI.lowAssign_subset line 21
4. lemma OAI.SeparableQuotient.ActualSpace.TypeI.lowAssign_disjoint line 25
5. def OAI.SeparableQuotient.ActualSpace.TypeI.boundaryDegree line 33
6. lemma OAI.SeparableQuotient.ActualSpace.TypeI.boundaryDegree_nonneg line 36
7. lemma OAI.SeparableQuotient.ActualSpace.TypeI.boundaryDegree_sum line 39
8. def OAI.SeparableQuotient.ActualSpace.TypeI.boundaryCharge line 49
9. lemma OAI.SeparableQuotient.ActualSpace.TypeI.boundaryCharge_nonneg line 54
10. lemma OAI.SeparableQuotient.ActualSpace.TypeI.boundaryCharge_norm line 61
11. lemma OAI.SeparableQuotient.ActualSpace.TypeI.low_eval_bound line 86
12. lemma OAI.SeparableQuotient.ActualSpace.Family.sum_theta_le line 134
13. lemma OAI.SeparableQuotient.ActualSpace.TypeII.group_theta_sum line 153
14. lemma OAI.SeparableQuotient.ActualSpace.TypeI.recombine_norm line 157
15. lemma OAI.SeparableQuotient.ActualSpace.TypeII.sum_vector_norm line 182
16. lemma OAI.SeparableQuotient.ActualSpace.TypeI.boundaryCharge_l1 line 201
17. lemma OAI.SeparableQuotient.ActualSpace.TypeII.sum_group_mask line 230
18. lemma OAI.SeparableQuotient.ActualSpace.TypeII.middle_group_sum line 241
19. lemma OAI.SeparableQuotient.ActualSpace.TypeII.eval_three_parts line 255
20. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.epsilon_pos line 276
21. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.middle_abs_bound line 284
22. lemma OAI.SeparableQuotient.ActualSpace.ThinnedWindows.node_split line 299