OAI/Combinatorics/Progressions/Probability/AnisotropicCanonicalDensity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coordinateRescaledDensity line 12
  2. theorem OAI.Erdos3.coordinateRescaledDensity_bound line 15
  3. theorem OAI.Erdos3.coordinateScale_lipschitz line 19
  4. theorem OAI.Erdos3.coordinateRescaledDensity_lipschitz line 31
  5. theorem OAI.Erdos3.maskedIntegerImageDensity_rescale line 37
  6. theorem OAI.Erdos3.diagonalDensityTransport_bound line 60
  7. theorem OAI.Erdos3.diagonalDensityTransport_lipschitz line 67
  8. theorem OAI.Erdos3.diagonalImageDensity_bound line 91
  9. theorem OAI.Erdos3.diagonalImageDensity_lipschitz line 98
  10. theorem OAI.Erdos3.diagonalImageDensity_zero_outside line 111
  11. def OAI.Erdos3.canonicalSpatialKernelDensity line 139
  12. def OAI.Erdos3.canonicalSpatialSiteDensity line 146
  13. theorem OAI.Erdos3.anisotropicSpatialKernelDensity_canonical line 154
  14. theorem OAI.Erdos3.canonicalSpatialSiteDensity_bounds line 178
  15. theorem OAI.Erdos3.anisotropicSpatial_mask_canonical line 210