OAI/Combinatorics/EuclideanRamsey/SmoothingKernel.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanRamsey.smoothPositivePart line 15
  2. def OAI.EuclideanRamsey.smoothPositivePart' line 17
  3. def OAI.EuclideanRamsey.smoothPositivePart'' line 19
  4. lemma OAI.EuclideanRamsey.smoothPositivePart_contDiff line 21
  5. lemma OAI.EuclideanRamsey.smoothPositivePart_hasDerivAt line 24
  6. lemma OAI.EuclideanRamsey.smoothPositivePart'_hasDerivAt line 37
  7. lemma OAI.EuclideanRamsey.smoothPositivePart_nonneg line 47
  8. lemma OAI.EuclideanRamsey.smoothPositivePart_pos line 52
  9. lemma OAI.EuclideanRamsey.smoothPositivePart_zero line 55
  10. lemma OAI.EuclideanRamsey.smoothPositivePart'_bounds line 58
  11. lemma OAI.EuclideanRamsey.smoothPositivePart''_nonneg line 71
  12. def OAI.EuclideanRamsey.radialPower line 80
  13. lemma OAI.EuclideanRamsey.radialPower_contDiff line 82
  14. lemma OAI.EuclideanRamsey.radialPower_hasFDerivAt line 87
  15. lemma OAI.EuclideanRamsey.radialPower_hessian line 98
  16. lemma OAI.EuclideanRamsey.scalarComposition_hessian line 118
  17. def OAI.EuclideanRamsey.halfLaplacian line 145
  18. lemma OAI.EuclideanRamsey.radialPower_halfLaplacian line 149
  19. def OAI.EuclideanRamsey.radialBump line 176
  20. lemma OAI.EuclideanRamsey.radialBump_contDiff line 180
  21. lemma OAI.EuclideanRamsey.radialBump_nonneg line 185
  22. lemma OAI.EuclideanRamsey.radialBump_compact line 188
  23. lemma OAI.EuclideanRamsey.radialBump_halfLaplacian line 197
  24. lemma OAI.EuclideanRamsey.smoothPositivePart_monotone line 242
  25. lemma OAI.EuclideanRamsey.radialBump_antitone_parameter line 247
  26. lemma OAI.EuclideanRamsey.radialBump_negative_le line 253
  27. def OAI.EuclideanRamsey.smoothingExponent line 272
  28. lemma OAI.EuclideanRamsey.smoothingExponent_neg line 275
  29. lemma OAI.EuclideanRamsey.radialPower_laplacian_lower line 280
  30. lemma OAI.EuclideanRamsey.radialPower_laplacian_nonneg_outside line 307
  31. lemma OAI.EuclideanRamsey.radialBump_weighted_negative_bound line 327
  32. lemma OAI.EuclideanRamsey.radialBump_integral_pos line 374
  33. lemma OAI.EuclideanRamsey.radialBump_integral_lower line 385
  34. lemma OAI.EuclideanRamsey.radial_weight_exponent line 397
  35. lemma OAI.EuclideanRamsey.radialBump_integral_negative_bound line 406
  36. theorem OAI.EuclideanRamsey.exists_radial_smoothing line 437