OAI/Combinatorics/Progressions/Lattices/AllocatedIntegerKernelComparison.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedPartitionedJetMatrix line 31
  2. def OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelPMF line 35
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelPMF_law line 40
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelPMF_reindexed line 57
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerProfileWidths_floor line 102
  6. def OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelDensity line 137
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelDensity_measurable line 144
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelDensity_probability_data line 156
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelDensity_bounds line 167
  10. theorem OAI.Erdos3.coefficientImagePMF_congr_scale line 197
  11. def OAI.Erdos3.VectorPolynomial.allocatedNonkernelJetMatrix line 233
  12. def OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelMask line 239
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelPMF_split_scale line 262
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernelDensity_of_matrix line 287
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerKernel_residue_family line 310