OAI/Combinatorics/Progressions/Estimates/RelativeRetainedCubeSource.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarCubeWeightPullbackMap line 13
  2. theorem OAI.Erdos3.scalarCubeWeightPullbackMap_lipschitz line 17
  3. theorem OAI.Erdos3.scalarCubeWeightPullback_lipschitz line 39
  4. theorem OAI.Erdos3.scalarCubeWeightPullbackMap_sample line 44
  5. theorem OAI.Erdos3.translatedCubeWeight_pullback line 57
  6. theorem OAI.Erdos3.scalarCubeWeightPullbackMap_lipschitz_of_width line 75
  7. theorem OAI.Erdos3.parentSliceWeight_lipschitz line 83
  8. theorem OAI.Erdos3.coefficientWeightPullbackMap_sample line 89
  9. def OAI.Erdos3.smoothCubeSliceOfPositiveIntegral line 121
  10. theorem OAI.Erdos3.smoothCubeSliceOfPositiveIntegral_law line 133
  11. def OAI.Erdos3.smoothCoefficientSliceOfPositiveIntegral line 156
  12. theorem OAI.Erdos3.smoothCoefficientSliceOfPositiveIntegral_law line 167
  13. def OAI.Erdos3.retainedSmoothCubeSlice line 194
  14. def OAI.Erdos3.retainedSmoothCoefficientSlice line 213
  15. def OAI.Erdos3.parentRetainedSmoothCubeSlice line 241
  16. def OAI.Erdos3.parentRetainedSmoothCoefficientSlice line 264
  17. def OAI.Erdos3.parentRetainedCubeSource line 293
  18. theorem OAI.Erdos3.parentRetainedCubeSource_finiteSlice line 311
  19. theorem OAI.Erdos3.parentRetainedCubeSource_sliceWeight line 325
  20. def OAI.Erdos3.parentRetainedCoefficientSource line 336
  21. theorem OAI.Erdos3.parentRetainedCoefficientSource_finiteSlice line 354
  22. theorem OAI.Erdos3.parentRetainedCoefficientSource_sliceWeight line 364
  23. def OAI.Erdos3.RelativeProgression.coefficientSlice line 388
  24. theorem OAI.Erdos3.RelativeProgression.coefficientSlice_nonempty line 390
  25. def OAI.Erdos3.RelativeProgression.coefficientReference line 396
  26. abbrev OAI.Erdos3.RelativeProgression.CoefficientResidueLabel line 400
  27. def OAI.Erdos3.RelativeProgression.retainedCoefficientSource line 402
  28. theorem OAI.Erdos3.RelativeProgression.retainedCoefficientSource_length line 416
  29. theorem OAI.Erdos3.RelativeProgression.retainedCoefficientSource_finiteSlice line 423
  30. theorem OAI.Erdos3.RelativeProgression.retainedCoefficientSource_sliceWeight line 431
  31. def OAI.Erdos3.RelativeProgression.cubeReference line 454
  32. abbrev OAI.Erdos3.RelativeProgression.CubeResidueLabel line 458
  33. def OAI.Erdos3.RelativeProgression.retainedCubeSource line 460
  34. theorem OAI.Erdos3.RelativeProgression.retainedCubeSource_length line 475
  35. theorem OAI.Erdos3.RelativeProgression.retainedCubeSource_root line 483
  36. theorem OAI.Erdos3.RelativeProgression.retainedCubeSource_finiteSlice line 491
  37. theorem OAI.Erdos3.RelativeProgression.retainedCubeSource_sliceWeight line 507