OAI/Combinatorics/Progressions/Estimates/ActiveProfileNoise.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.coefficientProfileCenter_mul line 10
  2. theorem OAI.Erdos3.coefficientProfileWidth_mul line 16
  3. theorem OAI.Erdos3.principalProfileSize_mul line 24
  4. theorem OAI.Erdos3.tailProfileSize_mul line 29
  5. theorem OAI.Erdos3.bounded_mem_nonprincipalCoefficientSlots line 48
  6. theorem OAI.Erdos3.boundedProfileCenter_dilation line 72
  7. theorem OAI.Erdos3.boundedProfileWidth_dilation line 84
  8. theorem OAI.Erdos3.boundedProfile_polynomial_split line 105
  9. abbrev OAI.Erdos3.SamplerCoefficientSlot line 167
  10. abbrev OAI.Erdos3.PartitionedProfileNoiseIndex line 170
  11. def OAI.Erdos3.partitionedProfileInput line 175
  12. theorem OAI.Erdos3.partitionedProfileInput_principal line 182
  13. theorem OAI.Erdos3.partitionedProfileInput_source line 189
  14. def OAI.Erdos3.partitionedProfilePrincipal line 207
  15. def OAI.Erdos3.partitionedProfileConstant line 212
  16. def OAI.Erdos3.partitionedProfileTerms line 216
  17. def OAI.Erdos3.partitionedProfileJet line 220
  18. theorem OAI.Erdos3.partitionedProfileJet_eq line 231
  19. def OAI.Erdos3.unitProfilePrincipalSize line 298
  20. def OAI.Erdos3.unitProfileTailSize line 301
  21. def OAI.Erdos3.partitionedAllocatedProfileJet line 304
  22. theorem OAI.Erdos3.partitionedProfileJet_mul line 312
  23. theorem OAI.Erdos3.partitionedAllocatedProfileJet_scale line 332
  24. theorem OAI.Erdos3.unitProfilePrincipalSize_pos line 348
  25. theorem OAI.Erdos3.unitProfileTailSize_pos line 351
  26. theorem OAI.Erdos3.partitionedProfilePrincipal_unit_bounds line 355
  27. theorem OAI.Erdos3.partitionedProfilePrincipal_unit_sum line 374
  28. theorem OAI.Erdos3.partitionedProfileTail_unit_sum line 389
  29. def OAI.Erdos3.unitProfilePrincipalLowerBound line 415
  30. theorem OAI.Erdos3.unitProfilePrincipalLowerBound_pos line 418
  31. theorem OAI.Erdos3.unitProfilePrincipalLowerBound_le line 422
  32. theorem OAI.Erdos3.partitionedProfilePrincipal_uniform_lower_bound line 434
  33. theorem OAI.Erdos3.partitioned_profile_comparison line 455
  34. def OAI.Erdos3.partitionedIdealMap line 565
  35. theorem OAI.Erdos3.partitionedIdealMap_measurable line 574
  36. theorem OAI.Erdos3.partitionedAllocatedProfileJet_zero line 597
  37. def OAI.Erdos3.partitionedRegularizedIdeal line 608
  38. theorem OAI.Erdos3.partitionedRegularizedIdeal_measurable line 614
  39. theorem OAI.Erdos3.partitionedRegularizedIdeal_probability line 622
  40. theorem OAI.Erdos3.partitionedRegularizedIdeal_bounds line 632
  41. theorem OAI.Erdos3.partitioned_profile_comparison_below line 653
  42. abbrev OAI.Erdos3.ActiveProfileCoefficientIndex line 757
  43. def OAI.Erdos3.profileNoiseWithActive line 760
  44. theorem OAI.Erdos3.profileNoiseWithActive_active line 768
  45. theorem OAI.Erdos3.profileNoiseWithActive_abs_le line 776
  46. theorem OAI.Erdos3.profileNoiseWithActive_measurable line 790
  47. theorem OAI.Erdos3.partitionedIdealMap_withActive_eq line 803
  48. theorem OAI.Erdos3.partitionedRegularizedIdeal_withActive_eq line 824