OAI/Combinatorics/Progressions/Estimates/RegularCylinderDecomposition.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ProductCylinder.cut line 11
  2. def OAI.Erdos3.ProductCylinder.erase line 15
  3. theorem OAI.Erdos3.ProductCylinder.cut_add_erase line 19
  4. theorem OAI.Erdos3.ProductCylinder.cut_nonneg line 24
  5. theorem OAI.Erdos3.ProductCylinder.erase_nonneg line 29
  6. theorem OAI.Erdos3.ProductCylinder.cut_le line 34
  7. theorem OAI.Erdos3.ProductCylinder.erase_le line 39
  8. instance OAI.Erdos3.ProductCylinder.containsDecidable line 46
  9. theorem OAI.Erdos3.ProductCylinder.density_cut line 50
  10. theorem OAI.Erdos3.ProductCylinder.density_erase line 79
  11. theorem OAI.Erdos3.ProductCylinder.mass_erase_self line 93
  12. theorem OAI.Erdos3.ProductCylinder.mass_erase_le line 108
  13. inductive OAI.Erdos3.CylinderRemovalChain line 123
  14. theorem OAI.Erdos3.ProductCylinder.mass_cut_self line 150
  15. theorem OAI.Erdos3.ProductCylinder.section_cut line 160
  16. theorem OAI.Erdos3.ProductCylinder.normalizedSection_cut line 171
  17. theorem OAI.Erdos3.ProductCylinder.normalized_cut_bounds line 179
  18. def OAI.Erdos3.ProductCylinder.positiveCandidates line 198
  19. theorem OAI.Erdos3.ProductCylinder.mem_positiveCandidates line 202
  20. theorem OAI.Erdos3.ProductCylinder.positiveCandidates_card_le line 208
  21. theorem OAI.Erdos3.ProductCylinder.positiveCandidates_erase_card_lt line 213
  22. def OAI.Erdos3.removedCylinderWeights line 244
  23. theorem OAI.Erdos3.removedCylinderWeights_length line 249
  24. theorem OAI.Erdos3.removedCylinderWeights_zero line 255
  25. theorem OAI.Erdos3.removedCylinderWeights_pairwise line 270
  26. theorem OAI.Erdos3.exists_finite_cylinder_removal line 298
  27. theorem OAI.Erdos3.CylinderRemovalChain.decomposition line 356
  28. theorem OAI.Erdos3.CylinderRemovalChain.mem_mass_gt line 366
  29. theorem OAI.Erdos3.CylinderRemovalChain.nodup line 379
  30. theorem OAI.Erdos3.CylinderRemovalChain.removed_size_mass line 402
  31. theorem OAI.Erdos3.removedCylinderWeights_bounds line 433
  32. theorem OAI.Erdos3.exists_regular_cylinder_decomposition line 447