OAI/Combinatorics/Progressions/Estimates/AllocatedEnormousProfiles.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.canonicalPrincipal_normalization line 13
  2. theorem OAI.Erdos3.canonicalFrozenPrincipal_normalization line 27
  3. theorem OAI.Erdos3.principalTupleResidues_has_lift line 38
  4. theorem OAI.Erdos3.principalTupleNormalized_norm_le line 51
  5. theorem OAI.Erdos3.mappedPrincipal_normalized_bound line 61
  6. theorem OAI.Erdos3.goodScalarKernelTuple_mapped_control line 79
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.scaled_condition_complexMean line 115
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_disintegrate line 130
  9. theorem OAI.Erdos3.principalTuple_complex_disintegrate line 146
  10. def OAI.Erdos3.principalAxisLength line 172
  11. abbrev OAI.Erdos3.PrincipalAxisTuples line 176
  12. def OAI.Erdos3.principalAxisRestrict line 180
  13. def OAI.Erdos3.principalAxisJoin line 184
  14. theorem OAI.Erdos3.principalAxisRestrict_join_left line 189
  15. theorem OAI.Erdos3.principalAxisRestrict_join_right line 197
  16. theorem OAI.Erdos3.principalAxisJoin_restrict line 205
  17. def OAI.Erdos3.principalAxisPartitionEquiv line 212
  18. theorem OAI.Erdos3.principalTupleWeights_partition_weight line 225
  19. theorem OAI.Erdos3.principalTupleWeights_partition line 239
  20. theorem OAI.Erdos3.principalTupleWeights_partition_residues line 262
  21. theorem OAI.Erdos3.principalResidue_positive_witness line 292
  22. theorem OAI.Erdos3.principalRetained_test_comparison line 311
  23. theorem OAI.Erdos3.containedProgressionTupleMap_axisJoin line 403
  24. abbrev OAI.Erdos3.PrincipalAxisParameter line 433
  25. def OAI.Erdos3.partitionedPrincipalInput line 436
  26. theorem OAI.Erdos3.partitionedPrincipalInput_value line 445
  27. theorem OAI.Erdos3.partitionedPrincipalInput_cube line 457
  28. theorem OAI.Erdos3.partitionedPrincipalInput_normalized line 470
  29. theorem OAI.Erdos3.partitionedPrincipalInput_frozen_bound line 487
  30. theorem OAI.Erdos3.partitionedPrincipalInput_frozen_cube line 503
  31. def OAI.Erdos3.VectorPolynomial.allocatedGridAxis line 530
  32. instance OAI.Erdos3.VectorPolynomial.allocatedGridAxisDecidable line 534
  33. def OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides line 539
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_pos line 542
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_long line 546
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_long_restricted line 565
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipal_partition_residues line 575
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedGridAxis_jet_frozen line 597
  39. theorem OAI.Erdos3.principalIntervalLength_mul_scale_bounds line 623
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_active line 648
  41. abbrev OAI.Erdos3.VectorPolynomial.AllocatedFrozenCoefficients line 677
  42. abbrev OAI.Erdos3.VectorPolynomial.AllocatedLongCoefficients line 679
  43. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientSplit line 681
  44. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientAxisLaw line 686
  45. def OAI.Erdos3.VectorPolynomial.allocatedFrozenCoefficientSource line 691
  46. def OAI.Erdos3.VectorPolynomial.allocatedLongCoefficientSource line 694
  47. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientAxisLaw_probability line 697
  48. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenCoefficientSource_probability line 701
  49. theorem OAI.Erdos3.VectorPolynomial.allocatedLongCoefficientSource_probability line 707
  50. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientSplit_measurePreserving line 713
  51. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientReconstruct_measurePreserving line 721
  52. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientReconstruct_grid line 729
  53. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientReconstruct_long line 735
  54. def OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileCenters line 755
  55. def OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileWidths line 760
  56. def OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileScales line 772
  57. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileScales_pos line 776
  58. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileWidths_pos line 782
  59. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_active line 791
  60. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_principalScale line 795
  61. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_constant_width line 804
  62. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_profile_width_large line 824
  63. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerProfile_support line 845
  64. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_profile_sum_pos line 854
  65. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerProfile_normalizer line 862
  66. def OAI.Erdos3.VectorPolynomial.allocatedEnormousProfilePMF line 872
  67. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_coefficient_law line 881
  68. theorem OAI.Erdos3.VectorPolynomial.allocatedEnormous_image_law line 905