OAI/Combinatorics/Progressions/Probability/CanonicalZeroSpatialInputLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.canonicalZeroSpatialInputSource_sigma line 12
  2. theorem OAI.Erdos3.unitCoefficientSource_split line 28
  3. def OAI.Erdos3.canonicalZeroSpatialInputIndex line 41
  4. def OAI.Erdos3.canonicalZeroSpatialInputMap line 55
  5. theorem OAI.Erdos3.canonicalZeroSpatialKernelMap_measurable line 61
  6. theorem OAI.Erdos3.canonicalZeroSpatialInputMap_measurable line 68
  7. def OAI.Erdos3.canonicalZeroSpatialFlatIndex line 82
  8. theorem OAI.Erdos3.canonicalZeroSpatialInputMap_law line 89
  9. theorem OAI.Erdos3.canonicalZeroSpatialInputMap_integral_complex line 121