OAI/Combinatorics/Progressions/Probability/CanonicalZeroSpatialDensity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sigmaAxisWeight_output_bounds line 13
  2. theorem OAI.Erdos3.sigmaAxisWeight_zero_outside line 28
  3. def OAI.Erdos3.canonicalSpatialKernelMap line 61
  4. theorem OAI.Erdos3.canonicalSpatialKernelDensity_probability_data line 68
  5. theorem OAI.Erdos3.canonicalSpatialKernelDensity_image_law line 78
  6. theorem OAI.Erdos3.canonicalSpatialSiteDensity_eq_kernel line 88
  7. def OAI.Erdos3.canonicalZeroSpatialJointDensity line 101
  8. theorem OAI.Erdos3.canonicalZeroSpatialJointDensity_probability_data line 104
  9. theorem OAI.Erdos3.canonicalZeroSpatialJointDensity_image_law line 117
  10. theorem OAI.Erdos3.canonicalZeroSpatialJointDensity_bounds line 128
  11. theorem OAI.Erdos3.canonicalZeroSpatialJointDensity_zero_outside line 158