OAI/Combinatorics/Progressions/Probability/AllocatedFrozenJetDensity.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerMatrixRealDensity_affine_continuous line 13
  2. theorem OAI.Erdos3.mixedArrayImageDensity_continuous line 40
  3. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetImageDensity_continuous line 68
  4. theorem OAI.Erdos3.VectorPolynomial.canonicalCoveredArrayDensity_continuous line 76
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousKernelDensity_output_continuous line 119
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalRealJetDensity_eq line 138
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIntegerJetPMF_eq line 166
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridJetPMF_eq line 179
  9. def OAI.Erdos3.VectorPolynomial.allocatedGridJetFactor line 233
  10. def OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity line 240
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetFactor_mem_Icc line 244
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_mem_Icc line 254
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridDensityFactor_eq line 261
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongDensityFactor_eq line 276
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalMixedDensity_factorization line 296
  16. def OAI.Erdos3.VectorPolynomial.allocatedFrozenJetReference line 336
  17. instance OAI.Erdos3.VectorPolynomial.allocatedFrozenJetReference_sigmaFinite line 340
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetFactor_probability_data line 352
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetFactor_law line 364
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_probability_data line 379
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_law line 392