OAI/Combinatorics/Progressions/Linear/SpatialMatrixBlockWideProbability.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.spatialRankExponent line 12
  2. def OAI.Erdos3.spatialRankPolynomial line 16
  3. theorem OAI.Erdos3.spatialRankPolynomial_degree line 20
  4. theorem OAI.Erdos3.spatialRankPolynomial_eq line 28
  5. theorem OAI.Erdos3.spatialRankPolynomial_actual_eval line 34
  6. theorem OAI.Erdos3.spatialRankPolynomial_top line 45
  7. def OAI.Erdos3.spatialKernelRankSlot line 58
  8. theorem OAI.Erdos3.spatialKernelRankSlot_injective line 61
  9. theorem OAI.Erdos3.spatial_kernel_selected_sum line 66
  10. theorem OAI.Erdos3.spatial_kernel_selected_raw line 75
  11. theorem OAI.Erdos3.spatialRankPolynomial_kernel_selected line 92
  12. theorem OAI.Erdos3.spatialRankPolynomial_kernel_selected_top line 101
  13. theorem OAI.Erdos3.samplerLong_killCompl_common line 129
  14. theorem OAI.Erdos3.spatialRankPolynomial_kernel_selected_long line 136
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSpatialRankPolynomial_kernel_selected_long line 170
  16. def OAI.Erdos3.spatialNoiseRankSlot line 207
  17. theorem OAI.Erdos3.spatialNoiseRankSlot_injective line 211
  18. def OAI.Erdos3.resampleSpatialRankNoise line 218
  19. theorem OAI.Erdos3.resampleSpatialRankNoise_coordinate line 223
  20. theorem OAI.Erdos3.spatialRankNoise_selected_top line 240
  21. theorem OAI.Erdos3.spatialRankPolynomial_top_congr line 265
  22. theorem OAI.Erdos3.spatialRankPolynomial_conditioned_top_congr line 277
  23. theorem OAI.Erdos3.selectedResidueSmoothPMF_singleton_eq_residue line 298
  24. theorem OAI.Erdos3.selectedResidueSmoothWeight_singleton_index_mass_pos line 312
  25. theorem OAI.Erdos3.selectedResidueSmoothPMF_singleton_eq_independent_map line 322
  26. theorem OAI.Erdos3.selectedResidueSmoothPMF_independent_mixture line 336
  27. theorem OAI.Erdos3.allocatedSpatialRank_residue_width line 356
  28. theorem OAI.Erdos3.allocatedSpatialRank_scalar_law line 364
  29. theorem OAI.Erdos3.allocatedSpatialRank_scalar_mass_pos line 385
  30. theorem OAI.Erdos3.allocatedSpatialRank_index_mass_pos line 402
  31. theorem OAI.Erdos3.allocatedSpatialRank_scalar_law_of_cell_mass line 418
  32. abbrev OAI.Erdos3.SpatialMatrixBlockIndex line 443
  33. def OAI.Erdos3.spatialMatrixBlockSlot line 445
  34. def OAI.Erdos3.spatialMatrixNormalizedEntries line 460
  35. def OAI.Erdos3.spatialMatrixIndexCenter line 465
  36. def OAI.Erdos3.spatialMatrixIndexWidth line 469
  37. theorem OAI.Erdos3.spatialMatrixIndexWidth_pos line 473
  38. theorem OAI.Erdos3.spatialMatrixIndexMass_pos line 481
  39. theorem OAI.Erdos3.spatialMatrixNormalizedEntries_residue line 490
  40. theorem OAI.Erdos3.spatialMatrixIndexPMF_marginal line 500
  41. theorem OAI.Erdos3.spatialMatrixNormalizedEntries_residue_law line 512
  42. theorem OAI.Erdos3.spatialMatrixNormalizedEntries_singleton_law line 528
  43. theorem OAI.Erdos3.spatialMatrixNormalizedEntries_residue_expectation line 543
  44. theorem OAI.Erdos3.spatialMatrixNormalizedEntries_mixture_expectation line 560
  45. theorem OAI.Erdos3.spatialMatrixNormalizedEntries_mixture_event line 583
  46. def OAI.Erdos3.spatialMatrixBlockEquiv line 617
  47. def OAI.Erdos3.spatialMatrixBlockEntry line 622
  48. theorem OAI.Erdos3.spatialMatrixBlockEntry_apply line 631
  49. theorem OAI.Erdos3.spatialMatrixBlockEntry_symm line 634
  50. theorem OAI.Erdos3.spatialMatrixBlockEntry_reindex_eval line 638
  51. theorem OAI.Erdos3.spatialMatrixBlockEntry_disjoint line 643
  52. theorem OAI.Erdos3.shiftedSmoothProductPMF_reindex line 651
  53. theorem OAI.Erdos3.rectangularLatticePoint_reindex line 659
  54. theorem OAI.Erdos3.spatialMatrixBlock_normalized_law line 664
  55. theorem OAI.Erdos3.spatialMatrix_decide_eq_classical line 690
  56. def OAI.Erdos3.spatialMatrixBlockThreshold line 695
  57. theorem OAI.Erdos3.spatialMatrixBlockThreshold_pos line 698
  58. def OAI.Erdos3.spatialMatrixBlockBad line 702
  59. theorem OAI.Erdos3.spatialMatrixBlock_flat_bad_probability line 707
  60. theorem OAI.Erdos3.spatialMatrixBlock_residue_bad_probability line 735
  61. theorem OAI.Erdos3.spatialMatrixBlock_cellMass_pos line 758
  62. theorem OAI.Erdos3.spatialMatrixBlock_bad_probability line 767
  63. theorem OAI.Erdos3.spatialMatrixBlockThreshold_inverse_le_exp line 795
  64. theorem OAI.Erdos3.spatialMatrixBlock_bad_probability_of_exp_width line 801