OAI/Combinatorics/Progressions/Linear/ActualMarkedSlowKernelCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_bounded_subgroup_net line 19
2. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_bounded_kernel_net line 56
3. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_bounded_kernel_net_with_budget line 88
4. theorem OAI.Erdos3.exists_slow_kernel_net_geometry_budget line 142
5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_slow_kernel_freezing_net line 219
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_slow_kernel_cells line 275
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_uniform_slow_kernel_cells line 368
8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_actual_marked_slow_kernel_cells line 445