OAI/Combinatorics/Progressions/Linear/AllocatedModularRankFullProductLaw.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedPrincipalRankCenter line 23
  2. def OAI.Erdos3.VectorPolynomial.allocatedPrincipalRankWidth line 27
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalRankWidth_pos line 33
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalRankWidth_large line 40
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalRankMass_pos line 47
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerIntegerPMFs_principal_shiftedSmooth line 53
  7. abbrev OAI.Erdos3.VectorPolynomial.AllocatedFullSmoothCoefficientIndex line 78
  8. abbrev OAI.Erdos3.VectorPolynomial.AllocatedFullContinuousCoefficientIndex line 83
  9. def OAI.Erdos3.VectorPolynomial.allocatedFullCoefficientSplit line 87
  10. def OAI.Erdos3.VectorPolynomial.allocatedSmoothFullSlot line 105
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedSmoothFullSlot_injective line 114
  12. def OAI.Erdos3.VectorPolynomial.allocatedSmoothFullEmbedding line 142
  13. def OAI.Erdos3.VectorPolynomial.allocatedDeckFullSlot line 148
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedDeckFullSlot_injective line 152
  15. def OAI.Erdos3.VectorPolynomial.allocatedDeckFullEmbedding line 165
  16. def OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray line 169
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_noise line 176
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_deck line 182
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_integer line 188
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_continuous line 195
  21. def OAI.Erdos3.VectorPolynomial.allocatedReadFullSmooth line 202
  22. def OAI.Erdos3.VectorPolynomial.allocatedReadFullDeck line 208
  23. def OAI.Erdos3.VectorPolynomial.allocatedReadFullContinuous line 213
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_read line 218
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_reduce line 225
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedFullCoefficientSplit_selected line 240
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_refresh line 250
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedFullArray_refresh_selected line 271
  29. def OAI.Erdos3.VectorPolynomial.allocatedFullSmoothScalarPMF line 312
  30. def OAI.Erdos3.VectorPolynomial.allocatedSelectedSmoothCenter line 322
  31. def OAI.Erdos3.VectorPolynomial.allocatedSelectedSmoothWidth line 326
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedSmoothWidth_pos line 331
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedSmoothMass_pos line 339
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedFullSmoothScalarPMF_selected line 350
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedGridPrincipalRank_active line 373
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedFullSmoothProductPMF_factorization line 390
  37. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckScalar_uniform_map line 405
  38. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckScalar_uniform_symm_map line 418
  39. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckScalar_uniform_test line 431