OAI/Analysis/JiangSu/DimensionDrop/DimensionDropRestriction.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DimensionDropRelations.Witness.generated_closed line 19
2. instance OAI.DimensionDropRelations.Witness.generated_cstar line 22
3. instance OAI.DimensionDropRelations.Witness.(instance at line 25) line 25
4. instance OAI.DimensionDropRelations.Witness.(instance at line 26) line 26
5. instance OAI.DimensionDropRelations.Witness.(instance at line 27) line 27
6. instance OAI.DimensionDropRelations.Witness.(instance at line 28) line 28
7. lemma OAI.DimensionDropRelations.Witness.phi_mem line 29
8. lemma OAI.DimensionDropRelations.Witness.s_mem line 31
9. def OAI.DimensionDropRelations.Witness.restrictPhi line 33
10. def OAI.DimensionDropRelations.Witness.restrict line 38
11. lemma OAI.DimensionDropRelations.Witness.restrict_image_generators line 45
12. theorem OAI.DimensionDropRelations.Witness.restrict_generated line 60
13. def OAI.DimensionDropModel.functionValues line 95
14. lemma OAI.DimensionDropModel.realization_eq_eval line 96
15. def OAI.DimensionDropModel.generated line 105
16. theorem OAI.DimensionDropRelations.Witness.polynomial_norm line 115
17. lemma OAI.DimensionDropModel.phi_amplify line 134
18. lemma OAI.DimensionDropModel.s_amplify line 137
19. lemma OAI.DimensionDropModel.upper_mul_bridge line 139
20. lemma OAI.DimensionDropModel.phi_mul_s line 143
21. lemma OAI.DimensionDropModel.s_mul_star line 146
22. lemma OAI.DimensionDropModel.sum_blocks line 151
23. theorem OAI.DimensionDropModel.parameter_formula line 159