OAI/Combinatorics/Progressions/Estimates/ProgressionCubeEmbedding.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.shiftScalarCubeResidues_neg_cancel line 13
  2. abbrev OAI.Erdos3.NormalizedScalarCubeSource.SliceDomain line 21
  3. theorem OAI.Erdos3.NormalizedScalarCubeSource.baseLaw_slice_mean line 24
  4. def OAI.Erdos3.NormalizedScalarCubeSource.sliceDensity line 32
  5. theorem OAI.Erdos3.NormalizedScalarCubeSource.sliceDensity_nonneg line 36
  6. theorem OAI.Erdos3.NormalizedScalarCubeSource.sliceDensity_mean_one line 39
  7. def OAI.Erdos3.NormalizedScalarCubeSource.sliceWeights line 44
  8. theorem OAI.Erdos3.NormalizedScalarCubeSource.source_slice_mean line 48
  9. theorem OAI.Erdos3.NormalizedScalarCubeSource.source_slice_complexMean line 60
  10. structure OAI.Erdos3.FiniteCubeSlice line 80
  11. abbrev OAI.Erdos3.FiniteCubeSlice.Domain line 88
  12. def OAI.Erdos3.FiniteCubeSlice.coordinates line 91
  13. def OAI.Erdos3.FiniteCubeSlice.radius line 94
  14. theorem OAI.Erdos3.FiniteCubeSlice.coordinates_abs_le line 96
  15. theorem OAI.Erdos3.FiniteCubeSlice.radius_relative line 119
  16. def OAI.Erdos3.cubeSliceEmbedding line 137
  17. theorem OAI.Erdos3.cubeSliceEmbedding_coordinates line 146
  18. def OAI.Erdos3.cubeSliceEvent line 150
  19. theorem OAI.Erdos3.cubeSliceEmbedding_range line 156
  20. def OAI.Erdos3.conditionCubeSlice line 172
  21. theorem OAI.Erdos3.conditionCubeSlice_complexMean line 179
  22. theorem OAI.Erdos3.uniform_condition_cubeSlice_mean line 189
  23. def OAI.Erdos3.FiniteCubeSlice.domainEquiv line 215
  24. theorem OAI.Erdos3.FiniteCubeSlice.coordinates_domainEquiv line 218
  25. def OAI.Erdos3.FiniteCoefficientSlice.domainEquiv line 227
  26. theorem OAI.Erdos3.FiniteCoefficientSlice.value_domainEquiv line 230
  27. theorem OAI.Erdos3.FiniteCoefficientSlice.index_domainEquiv line 235
  28. structure OAI.Erdos3.RetainedCubeSlice line 252
  29. def OAI.Erdos3.RetainedCubeSlice.finiteSlice line 270
  30. abbrev OAI.Erdos3.RetainedCubeSlice.Domain line 276
  31. def OAI.Erdos3.RetainedCubeSlice.sliceWeight line 278
  32. theorem OAI.Erdos3.RetainedCubeSlice.sliceWeight_nonneg line 281
  33. theorem OAI.Erdos3.RetainedCubeSlice.total_pos line 283
  34. def OAI.Erdos3.RetainedCubeSlice.law line 286
  35. theorem OAI.Erdos3.RetainedCubeSlice.length_pos_of_size line 289
  36. def OAI.Erdos3.RetainedCubeSlice.normalizer line 293
  37. theorem OAI.Erdos3.RetainedCubeSlice.normalizer_eq_mean line 298
  38. theorem OAI.Erdos3.RetainedCubeSlice.normalizer_lower line 312
  39. def OAI.Erdos3.RetainedCubeSlice.normalized line 316
  40. theorem OAI.Erdos3.RetainedCubeSlice.normalized_sliceDensity line 322
  41. theorem OAI.Erdos3.RetainedCubeSlice.normalized_sliceWeights line 326
  42. structure OAI.Erdos3.SmoothCubeSlice line 345
  43. def OAI.Erdos3.SmoothCubeSlice.finiteSlice line 361
  44. abbrev OAI.Erdos3.SmoothCubeSlice.Domain line 367
  45. def OAI.Erdos3.SmoothCubeSlice.sliceWeight line 369
  46. theorem OAI.Erdos3.SmoothCubeSlice.sliceWeight_nonneg line 372
  47. def OAI.Erdos3.SmoothCubeSlice.law line 374
  48. def OAI.Erdos3.SmoothCubeSlice.longNormalizer line 377
  49. theorem OAI.Erdos3.SmoothCubeSlice.longNormalizer_bounds line 383
  50. theorem OAI.Erdos3.SmoothCubeSlice.longNormalizer_eq_expect line 388
  51. theorem OAI.Erdos3.SmoothCubeSlice.long_total_pos line 404
  52. def OAI.Erdos3.SmoothCubeSlice.normalized line 411
  53. theorem OAI.Erdos3.SmoothCubeSlice.normalized_sliceDensity line 416
  54. theorem OAI.Erdos3.SmoothCubeSlice.normalized_sliceWeights line 420
  55. def OAI.Erdos3.supportedCubeInclusion line 437
  56. def OAI.Erdos3.progressionCubeSlice line 444
  57. def OAI.Erdos3.progressionCubeSliceEmbedding line 450
  58. theorem OAI.Erdos3.progressionCubeSliceEmbedding_coordinates line 455
  59. theorem OAI.Erdos3.progressionCubeSliceEmbedding_range line 461