OAI/Analysis/HotSpots/KernelLimit.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.L2Cutoff.extension_memLp line 16
  2. def OAI.StrictHotSpots.L2Cutoff.extension line 19
  3. lemma OAI.StrictHotSpots.L2Cutoff.extension_ae line 50
  4. lemma OAI.StrictHotSpots.L2Cutoff.extension_norm line 53
  5. lemma OAI.StrictHotSpots.L2Cutoff.extension_norm_le line 58
  6. def OAI.StrictHotSpots.L2Cutoff.restriction line 63
  7. lemma OAI.StrictHotSpots.L2Cutoff.restriction_ae line 67
  8. lemma OAI.StrictHotSpots.L2Cutoff.restriction_norm line 70
  9. lemma OAI.StrictHotSpots.L2Cutoff.restriction_norm_le line 75
  10. lemma OAI.StrictHotSpots.L2Cutoff.restriction_extension line 80
  11. lemma OAI.StrictHotSpots.L2Cutoff.extension_inner line 87
  12. lemma OAI.StrictHotSpots.L2Cutoff.extension_eq_adjoint line 100
  13. lemma OAI.StrictHotSpots.L2Cutoff.extension_inner_extension line 103
  14. def OAI.StrictHotSpots.L2Cutoff.projection line 107
  15. lemma OAI.StrictHotSpots.L2Cutoff.projection_ae line 109
  16. lemma OAI.StrictHotSpots.L2Cutoff.projection_norm line 118
  17. lemma OAI.StrictHotSpots.L2Cutoff.projection_norm_le line 121
  18. lemma OAI.StrictHotSpots.L2Cutoff.projection_idempotent line 126
  19. lemma OAI.StrictHotSpots.L2Cutoff.projection_symmetric line 130
  20. lemma OAI.StrictHotSpots.L2Cutoff.projection_tendsto line 151
  21. lemma OAI.StrictHotSpots.BanachResolvent.bounded_strong_tendsto_moving line 172
  22. lemma OAI.StrictHotSpots.BanachResolvent.compression_norm_le line 186
  23. lemma OAI.StrictHotSpots.BanachResolvent.compression_strong_tendsto line 196
  24. def OAI.StrictHotSpots.L2Cutoff.restrictedOperator line 215
  25. def OAI.StrictHotSpots.L2Cutoff.compressedOperator line 219
  26. lemma OAI.StrictHotSpots.L2Cutoff.restrictedOperator_norm_le line 222
  27. lemma OAI.StrictHotSpots.L2Cutoff.compressedOperator_norm_le line 233
  28. lemma OAI.StrictHotSpots.L2Cutoff.extension_intertwine line 237
  29. lemma OAI.StrictHotSpots.L2Cutoff.resolvent_extension line 244
  30. lemma OAI.StrictHotSpots.L2Cutoff.resolvent_inner_extension line 255
  31. lemma OAI.StrictHotSpots.PlaneGreen.restrictDensity line 269
  32. lemma OAI.StrictHotSpots.PlaneGreen.inclusion_restrict line 272
  33. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_restrict line 282
  34. lemma OAI.StrictHotSpots.PlaneGreen.weightedValue_restrict line 289
  35. lemma OAI.StrictHotSpots.PlaneGreen.subcritical_restrict line 294
  36. lemma OAI.StrictHotSpots.PlaneGreen.row_restrict line 303
  37. def OAI.StrictHotSpots.PlaneGreen.cutoffRadius line 321
  38. def OAI.StrictHotSpots.PlaneGreen.cutoffSet line 322
  39. lemma OAI.StrictHotSpots.PlaneGreen.cutoffRadius_nonneg line 324
  40. lemma OAI.StrictHotSpots.PlaneGreen.cutoffRadius_lt_one line 330
  41. lemma OAI.StrictHotSpots.PlaneGreen.cutoffRadius_tendsto line 334
  42. lemma OAI.StrictHotSpots.PlaneGreen.cutoffSet_compact line 339
  43. lemma OAI.StrictHotSpots.PlaneGreen.cutoffSet_measurable line 340
  44. lemma OAI.StrictHotSpots.PlaneGreen.cutoffSet_subset line 341
  45. lemma OAI.StrictHotSpots.PlaneGreen.eventually_mem_cutoffSet line 346
  46. lemma OAI.StrictHotSpots.PlaneGreen.ae_eventually_mem_cutoffSet line 356
  47. lemma OAI.StrictHotSpots.PlaneGreen.cutoffProjection_tendsto line 361
  48. lemma OAI.StrictHotSpots.PlaneGreen.cutoff_integral_tendsto line 367
  49. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_nonneg line 383
  50. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_restrict_le line 390
  51. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_full_memLp line 397
  52. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_cutoff_tendsto line 407
  53. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_cutoff_L2_tendsto line 412
  54. lemma OAI.StrictHotSpots.BanachResolvent.apply_eq_add line 438
  55. lemma OAI.StrictHotSpots.BanachResolvent.apply_eq_add_left line 446
  56. lemma OAI.StrictHotSpots.BanachResolvent.inner_two_terms line 454
  57. def OAI.StrictHotSpots.PlaneGreen.smoothedRow line 471
  58. def OAI.StrictHotSpots.PlaneGreen.cutoffSmoothedRow line 474
  59. lemma OAI.StrictHotSpots.PlaneGreen.cutoff_ae_norm line 479
  60. lemma OAI.StrictHotSpots.PlaneGreen.compactSmoothedRow_eq line 483
  61. lemma OAI.StrictHotSpots.PlaneGreen.extendedSmoothedRow_tendsto line 499
  62. def OAI.StrictHotSpots.PlaneGreen.fullBoundaryK line 511
  63. def OAI.StrictHotSpots.PlaneGreen.fullBoundaryN line 517
  64. lemma OAI.StrictHotSpots.PlaneGreen.smoothedRow_nonneg line 523
  65. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryK_pos line 529
  66. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryN_pos line 537
  67. lemma OAI.StrictHotSpots.PlaneGreen.poisson_measurable line 563
  68. lemma OAI.StrictHotSpots.PlaneGreen.poisson_invnorm_bound line 567
  69. lemma OAI.StrictHotSpots.PlaneGreen.poisson_product_bound line 573
  70. lemma OAI.StrictHotSpots.PlaneGreen.poisson_integrable line 607
  71. lemma OAI.StrictHotSpots.PlaneGreen.poisson_product_integrable line 611
  72. lemma OAI.StrictHotSpots.PlaneGreen.poisson_smoothed_integrable line 622
  73. lemma OAI.StrictHotSpots.PlaneGreen.poisson_smoothed_cutoff_tendsto line 633
  74. abbrev OAI.StrictHotSpots.PlaneGreen.cutoffOperator line 678
  75. abbrev OAI.StrictHotSpots.PlaneGreen.cutoffK line 681
  76. abbrev OAI.StrictHotSpots.PlaneGreen.cutoffN line 685
  77. lemma OAI.StrictHotSpots.PlaneGreen.cutoff_row_inner line 689
  78. lemma OAI.StrictHotSpots.PlaneGreen.cutoff_poisson_inner line 702
  79. lemma OAI.StrictHotSpots.PlaneGreen.cutoff_poisson_smoothed_inner line 710
  80. lemma OAI.StrictHotSpots.PlaneGreen.cutoffK_expansion line 728
  81. lemma OAI.StrictHotSpots.PlaneGreen.cutoffN_expansion line 752
  82. lemma OAI.StrictHotSpots.PlaneGreen.cutoffOperator_strong_tendsto line 782
  83. lemma OAI.StrictHotSpots.PlaneGreen.cutoff_resolvent_smoothed_tendsto line 787
  84. lemma OAI.StrictHotSpots.PlaneGreen.cutoffK_tendsto line 796
  85. lemma OAI.StrictHotSpots.PlaneGreen.cutoffN_tendsto line 804
  86. theorem OAI.StrictHotSpots.PlaneGreen.boundary_reciprocal line 827
  87. def OAI.StrictHotSpots.PlaneGreen.fullDistanceKernel line 861
  88. theorem OAI.StrictHotSpots.PlaneGreen.negative_kernel line 867
  89. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryK_bounded line 911
  90. lemma OAI.StrictHotSpots.PlaneGreen.boundaryInteraction_eq_dist line 938
  91. lemma OAI.StrictHotSpots.PlaneGreen.boundaryInteraction_le_fullBoundaryN line 943
  92. lemma OAI.StrictHotSpots.PlaneGreen.fullDistanceKernel_pos line 959
  93. lemma OAI.StrictHotSpots.PlaneGreen.fullDistanceKernel_bound line 965
  94. lemma OAI.StrictHotSpots.PlaneGreen.fullDistanceKernel_conditionallyNegative line 989
  95. theorem OAI.StrictHotSpots.PlaneGreen.full_boundary_hilbert_embedding line 1022