OAI/Combinatorics/Progressions/Linear/AllocatedModularRankMixedUniform.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.modularBoundedCoefficientPolynomial_booleanCoefficient line 11
  2. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_eq_booleanCoefficient line 42
  3. def OAI.Erdos3.VectorPolynomial.modularDeckPolynomial line 73
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_eq_modularDeckPolynomial line 77
  5. theorem OAI.Erdos3.VectorPolynomial.modularDeckPolynomial_degree line 87
  6. def OAI.Erdos3.VectorPolynomial.resampleCoefficientDeckCoordinate line 93
  7. theorem OAI.Erdos3.VectorPolynomial.resampleCoefficientDeckCoordinate_apply line 101
  8. theorem OAI.Erdos3.VectorPolynomial.resampleCoefficientDeckCoordinate_selected line 110
  9. theorem OAI.Erdos3.VectorPolynomial.modularDeckPolynomial_resample_top line 117
  10. theorem OAI.Erdos3.samplerLongEmbedding_kernelExponent line 133
  11. theorem OAI.Erdos3.VectorPolynomial.modularDeckPolynomial_kernel_resample_top line 150
  12. theorem OAI.Erdos3.VectorPolynomial.modularDeckPolynomial_kernel_resample_long_top line 165
  13. abbrev OAI.Erdos3.VectorPolynomial.CoefficientDeckScalarIndex line 208
  14. def OAI.Erdos3.VectorPolynomial.coefficientDeckScalarEquiv line 211
  15. def OAI.Erdos3.VectorPolynomial.coefficientDeckSelectedEmbedding line 218
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckScalarEquiv_resample line 228
  17. theorem OAI.Erdos3.VectorPolynomial.expect_resampleCoefficientDeckCoordinate line 279
  18. theorem OAI.Erdos3.VectorPolynomial.expect_coefficientDeck_selected line 303
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientDeck_expect_le_of_resampling line 314
  20. abbrev OAI.Erdos3.VectorPolynomial.AllocatedProjectionCoefficientIndex line 339
  21. abbrev OAI.Erdos3.VectorPolynomial.AllocatedActualCoefficientIndex line 342
  22. abbrev OAI.Erdos3.VectorPolynomial.AllocatedSelectedCoefficientIndex line 348
  23. def OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientSlot line 352
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientSlot_injective line 363
  25. def OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientEmbedding line 427
  26. def OAI.Erdos3.VectorPolynomial.allocatedReadNoise line 437
  27. def OAI.Erdos3.VectorPolynomial.allocatedReadDeck line 441
  28. def OAI.Erdos3.VectorPolynomial.allocatedReadProjection line 445
  29. def OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientEquiv line 450
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientSlot_read_spatial line 467
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientSlot_read_deck line 476
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedActualCoefficientSlot_read_projection line 485
  33. def OAI.Erdos3.VectorPolynomial.resampleCoefficientDeckLayer line 507
  34. theorem OAI.Erdos3.VectorPolynomial.resampleCoefficientDeckLayer_apply line 513
  35. theorem OAI.Erdos3.VectorPolynomial.resampleCoefficientDeckLayer_selected line 521
  36. theorem OAI.Erdos3.VectorPolynomial.modularDeckPolynomial_resampleLayer line 528
  37. theorem OAI.Erdos3.VectorPolynomial.exists_coefficientDeck_layer_witness line 537
  38. def OAI.Erdos3.VectorPolynomial.coefficientDeckLayerSelectedEmbedding line 545
  39. def OAI.Erdos3.VectorPolynomial.coefficientDeckLayerFreshEquiv line 555
  40. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckScalarEquiv_resampleLayer line 562
  41. theorem OAI.Erdos3.VectorPolynomial.expect_resampleCoefficientDeckLayer line 603
  42. theorem OAI.Erdos3.VectorPolynomial.expect_coefficientDeck_layer_selected line 627
  43. theorem OAI.Erdos3.VectorPolynomial.expect_allocatedActualCoefficient_selected line 659
  44. theorem OAI.Erdos3.VectorPolynomial.expect_allocatedActualCoefficient_resample line 672
  45. theorem OAI.Erdos3.VectorPolynomial.expect_allocatedActualCoefficient_selected_subfamily line 684
  46. abbrev OAI.Erdos3.VectorPolynomial.AllocatedCongruenceCoefficientIndex line 709
  47. abbrev OAI.Erdos3.VectorPolynomial.AllocatedSmoothRankCoefficientIndex line 713
  48. abbrev OAI.Erdos3.VectorPolynomial.AllocatedDeckRankCoefficientIndex line 717
  49. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceCoefficientSplit line 720
  50. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceCoefficientEmbedding line 734
  51. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceActualCoefficientEmbedding line 741
  52. def OAI.Erdos3.VectorPolynomial.allocatedMixedSelectedValues line 749
  53. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedSelectedValues_spatial line 755
  54. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedSelectedValues_deck line 761
  55. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedSelectedValues_integer line 767
  56. def OAI.Erdos3.VectorPolynomial.AllocatedRankComponentCoefficient line 786
  57. abbrev OAI.Erdos3.VectorPolynomial.AllocatedRankComponentCoefficientIndex line 792
  58. def OAI.Erdos3.VectorPolynomial.allocatedRankComponentCoefficientSlot line 798
  59. theorem OAI.Erdos3.VectorPolynomial.allocatedRankComponentCoefficientSlot_injective line 806
  60. def OAI.Erdos3.VectorPolynomial.allocatedRankComponentCoefficientEmbedding line 861
  61. def OAI.Erdos3.VectorPolynomial.allocatedRankComponentSelectedSlot line 868
  62. theorem OAI.Erdos3.VectorPolynomial.allocatedRankComponentSelectedSlot_injective line 879
  63. def OAI.Erdos3.VectorPolynomial.allocatedRankComponentSelectedEmbedding line 893
  64. theorem OAI.Erdos3.VectorPolynomial.allocatedRankComponentCoefficientEmbedding_selected line 902
  65. def OAI.Erdos3.VectorPolynomial.allocatedMixedCoefficientEquiv line 923
  66. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedCoefficient_uniform_event line 941
  67. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedCoefficientEquiv_cast line 954