OAI/Combinatorics/Progressions/Estimates/AllocatedTailProfileIdentity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.partitionedSlicedRegularizedIdeal line 17
  2. theorem OAI.Erdos3.partitionedSlicedIdealMap_measurable line 24
  3. theorem OAI.Erdos3.partitionedSlicedRegularizedIdeal_measurable line 48
  4. theorem OAI.Erdos3.partitionedSlicedIdealMap_measurable_fixed line 58
  5. theorem OAI.Erdos3.partitionedSlicedRegularizedIdeal_probability line 68
  6. theorem OAI.Erdos3.partitionedSlicedRegularizedIdeal_bounds line 77
  7. def OAI.Erdos3.activeTailRescale line 101
  8. theorem OAI.Erdos3.activeTailRescale_principal line 106
  9. theorem OAI.Erdos3.activeTailRescale_constant line 114
  10. theorem OAI.Erdos3.activeTailRescale_abs_le line 122
  11. theorem OAI.Erdos3.activeTailRescale_measurable_comp line 135
  12. theorem OAI.Erdos3.partitionedIdealMap_activeTailRescale line 141
  13. theorem OAI.Erdos3.partitionedRegularizedIdeal_activeTailRescale line 161
  14. theorem OAI.Erdos3.boundedProfileWidth_noise_rescale line 171
  15. def OAI.Erdos3.activeSlicedProfileIdeal line 207
  16. theorem OAI.Erdos3.activeSlicedProfileIdeal_measurable line 213
  17. def OAI.Erdos3.activeAveragedSlicedProfileIdeal line 222
  18. theorem OAI.Erdos3.activeAveragedSlicedProfileIdeal_spec line 228
  19. theorem OAI.Erdos3.partitionedSlicedRegularizedIdeal_activeTailRescale line 250
  20. def OAI.Erdos3.activeTailProfileSample line 272
  21. theorem OAI.Erdos3.exists_active_tail_profile_comparison line 284
  22. def OAI.Erdos3.activeAveragedSlicedIdealSiteFunction line 396
  23. theorem OAI.Erdos3.activeAveragedSlicedIdealSiteFunction_bound line 400
  24. theorem OAI.Erdos3.activeAveragedSlicedIdealSiteFunction_lipschitz line 409
  25. theorem OAI.Erdos3.exists_active_sliced_ideal_site_approximation line 431
  26. def OAI.Erdos3.VectorPolynomial.allocatedProfileFrozenNoise line 502
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedProfileFrozenNoise_abs_le line 506
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedTailRatio_abs_le line 514
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedTailProfileJet_eq line 523