OAI/Combinatorics/Progressions/Estimates/AllocatedRelativeChildSliceGeometry.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedSampleNormalizedCoefficients line 28
  2. def OAI.Erdos3.VectorPolynomial.allocatedSampleProfileNoise line 33
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleProfileNoise_polynomial line 43
  4. def OAI.Erdos3.VectorPolynomial.allocatedSampleActiveProfileNoise line 63
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleActiveProfileNoise_measurable line 67
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPrincipal_of_sample line 82
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathShift_of_sample line 96
  8. theorem OAI.Erdos3.VectorPolynomial.normalized_profile_noise_abs_le line 108
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleProfileNoise_continuous_bound line 116
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleProfileNoise_integer_bound line 142
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleActiveProfileNoise_abs_le line 153
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleActiveProfileNoise_ae_abs_le line 168
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleNormalizedCoefficients_continuous line 184
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleNormalizedCoefficients_integer line 190
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleProfileNoise_active_integer_coordinate_bound line 220
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleProfileNoise_active_integer_bound line 256
  17. def OAI.Erdos3.VectorPolynomial.allocatedShortAxis line 288
  18. instance OAI.Erdos3.VectorPolynomial.allocatedShortAxisDecidable line 292
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_long_of_not_short line 295
  20. def OAI.Erdos3.VectorPolynomial.allocatedSampleRestrictedProfileNoise line 309
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedSampleRestrictedProfileNoise_measurable line 313
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPrincipal_of_restricted_sample line 328
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathShift_of_restricted_sample line 342
  24. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePrincipal line 381
  25. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleShift line 385
  26. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap line 392
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_apply line 396
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSamplePrincipal_eq_fixedPath line 407
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleShift_eq_fixedPath line 415
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_eq_fixedPath line 423
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftMap_measurable line 432
  32. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceSubstitution line 477
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceSubstitution_principal line 485
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceSubstitution_degree line 492
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceSubstitution_mass line 503
  36. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceInput line 526
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleSliceSubstitution_eval line 532
  38. def OAI.Erdos3.VectorPolynomial.allocatedChildKernelCoordinate line 563
  39. def OAI.Erdos3.VectorPolynomial.allocatedChildActiveCoordinate line 566
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedChildActiveCoordinate_side line 576
  41. theorem OAI.Erdos3.VectorPolynomial.allocatedChildSlice_long_coordinate_geometry line 584
  42. theorem OAI.Erdos3.VectorPolynomial.allocatedChildSlice_kernel_geometry line 599
  43. theorem OAI.Erdos3.VectorPolynomial.allocatedChildSlice_active_geometry line 614
  44. theorem OAI.Erdos3.VectorPolynomial.allocatedChildSlice_stride_le line 632
  45. def OAI.Erdos3.VectorPolynomial.allocatedChildNonshortCoordinate line 642
  46. theorem OAI.Erdos3.VectorPolynomial.allocatedChildNonshortCoordinate_side line 651
  47. theorem OAI.Erdos3.VectorPolynomial.allocatedChildSlice_nonshort_geometry line 657