OAI/Analysis/HotSpots/DiskKernel.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.ScalarKernel.choose_recurrence line 14
  2. def OAI.StrictHotSpots.ScalarKernel.coeff line 26
  3. lemma OAI.StrictHotSpots.ScalarKernel.coeff_nonneg line 28
  4. lemma OAI.StrictHotSpots.ScalarKernel.binomial_hasSum line 46
  5. lemma OAI.StrictHotSpots.ScalarKernel.defect_hasSum line 54
  6. lemma OAI.StrictHotSpots.ScalarKernel.posSemidef_entry_pow line 79
  7. lemma OAI.StrictHotSpots.ScalarKernel.posSemidef_of_entrywise_tendsto line 94
  8. lemma OAI.StrictHotSpots.ScalarKernel.defect_posSemidef line 112
  9. lemma OAI.StrictHotSpots.ScalarKernel.integral_posSemidef line 126
  10. lemma OAI.StrictHotSpots.ScalarKernel.integral_rpow_parameter line 159
  11. lemma OAI.StrictHotSpots.ScalarKernel.integral_defect line 169
  12. lemma OAI.StrictHotSpots.ScalarKernel.logDefect_posSemidef line 192
  13. def OAI.StrictHotSpots.ScalarKernel.dilation line 206
  14. lemma OAI.StrictHotSpots.ScalarKernel.dilation_pos line 208
  15. lemma OAI.StrictHotSpots.ScalarKernel.dilation_lt_one line 212
  16. lemma OAI.StrictHotSpots.ScalarKernel.dilation_tendsto line 217
  17. lemma OAI.StrictHotSpots.ScalarKernel.invLog_continuousAt_zero line 224
  18. lemma OAI.StrictHotSpots.ScalarKernel.logDefect_tendsto line 229
  19. lemma OAI.StrictHotSpots.ScalarKernel.logDefect_posSemidef_le line 246
  20. abbrev OAI.StrictHotSpots.DiskKernel.Disk line 271
  21. def OAI.StrictHotSpots.DiskKernel.h line 273
  22. def OAI.StrictHotSpots.DiskKernel.logMean line 276
  23. def OAI.StrictHotSpots.DiskKernel.f line 278
  24. def OAI.StrictHotSpots.DiskKernel.green line 281
  25. def OAI.StrictHotSpots.DiskKernel.greenExtended line 285
  26. def OAI.StrictHotSpots.DiskKernel.regularized line 289
  27. lemma OAI.StrictHotSpots.DiskKernel.disk_weight_pos line 292
  28. lemma OAI.StrictHotSpots.DiskKernel.h_nonneg line 297
  29. lemma OAI.StrictHotSpots.DiskKernel.h_pos line 300
  30. lemma OAI.StrictHotSpots.DiskKernel.h_self line 304
  31. lemma OAI.StrictHotSpots.DiskKernel.logMean_zero line 305
  32. lemma OAI.StrictHotSpots.DiskKernel.f_zero line 306
  33. lemma OAI.StrictHotSpots.DiskKernel.complex_posSemidef_of_entrywise_tendsto line 308
  34. lemma OAI.StrictHotSpots.DiskKernel.szego_posSemidef line 325
  35. lemma OAI.StrictHotSpots.DiskKernel.realPart_posSemidef line 342
  36. lemma OAI.StrictHotSpots.DiskKernel.disk_cross_identity line 353
  37. lemma OAI.StrictHotSpots.DiskKernel.normSzego_posSemidef line 360
  38. lemma OAI.StrictHotSpots.DiskKernel.k_identity line 373
  39. lemma OAI.StrictHotSpots.DiskKernel.k_posSemidef line 383
  40. lemma OAI.StrictHotSpots.DiskKernel.f_eq_logDefect line 396
  41. lemma OAI.StrictHotSpots.DiskKernel.f_posSemidef line 409
  42. lemma OAI.StrictHotSpots.DiskKernel.logMean_nonneg line 416
  43. lemma OAI.StrictHotSpots.DiskKernel.logMean_pos line 420
  44. lemma OAI.StrictHotSpots.DiskKernel.f_nonneg line 424
  45. lemma OAI.StrictHotSpots.DiskKernel.f_le_half line 438
  46. lemma OAI.StrictHotSpots.DiskKernel.f_alt line 455
  47. lemma OAI.StrictHotSpots.DiskKernel.f_continuousAt line 466
  48. lemma OAI.StrictHotSpots.DiskKernel.h_continuous line 480
  49. lemma OAI.StrictHotSpots.DiskKernel.regularized_denominator line 488
  50. lemma OAI.StrictHotSpots.DiskKernel.regularized_pos line 498
  51. lemma OAI.StrictHotSpots.DiskKernel.regularized_le line 504
  52. lemma OAI.StrictHotSpots.DiskKernel.regularized_continuous line 511
  53. lemma OAI.StrictHotSpots.DiskKernel.regularized_self line 524
  54. lemma OAI.StrictHotSpots.DiskKernel.regularized_antitone line 530
  55. lemma OAI.StrictHotSpots.DiskKernel.regularized_tendsto_offDiagonal line 539
  56. lemma OAI.ReciprocalKernel.onePositiveSquare_smul line 568
  57. lemma OAI.StrictHotSpots.DiskKernel.lorentz_identity line 587
  58. lemma OAI.StrictHotSpots.DiskKernel.regularized_reciprocal_onePositiveSquare line 599
  59. lemma OAI.StrictHotSpots.DiskKernel.regularized_zero line 652
  60. lemma OAI.StrictHotSpots.DiskKernel.regularized_le_green line 660
  61. lemma OAI.StrictHotSpots.DiskKernel.regularized_tendsto_diagonal line 672
  62. lemma OAI.StrictHotSpots.DiskKernel.regularized_tendsto line 680
  63. theorem OAI.StrictHotSpots.DiskKernel.bounded_green_regularization line 692