OAI/Analysis/HotSpots/BoundaryKernel.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.MeasureKernelTransfer.integral_mul_eq_inner line 16
  2. def OAI.StrictHotSpots.MeasureKernelTransfer.observe line 28
  3. lemma OAI.StrictHotSpots.MeasureKernelTransfer.observe_ae line 31
  4. lemma OAI.StrictHotSpots.MeasureKernelTransfer.observe_row line 34
  5. def OAI.StrictHotSpots.MeasureKernelTransfer.operator line 37
  6. lemma OAI.StrictHotSpots.MeasureKernelTransfer.integral_adjoint_row line 40
  7. lemma OAI.StrictHotSpots.MeasureKernelTransfer.operator_ae line 48
  8. lemma OAI.StrictHotSpots.MeasureKernelTransfer.observe_norm_le line 62
  9. lemma OAI.StrictHotSpots.MeasureKernelTransfer.operator_norm_le line 68
  10. lemma OAI.StrictHotSpots.MeasureKernelTransfer.observe_inner line 90
  11. lemma OAI.StrictHotSpots.MeasureKernelTransfer.adjoint_observe line 94
  12. lemma OAI.StrictHotSpots.MeasureKernelTransfer.operator_observe line 100
  13. lemma OAI.StrictHotSpots.MeasureKernelTransfer.resolvent_observe line 105
  14. lemma OAI.StrictHotSpots.MeasureKernelTransfer.resolvent_inner line 116
  15. lemma OAI.StrictHotSpots.DiskKernel.green_eq_formula line 129
  16. lemma OAI.StrictHotSpots.DiskKernel.regularized_symm line 135
  17. lemma OAI.StrictHotSpots.PlaneGreen.kernel_symm line 140
  18. def OAI.StrictHotSpots.DiskCompact.coordinates line 150
  19. lemma OAI.StrictHotSpots.DiskCompact.coordinates_continuous line 155
  20. lemma OAI.StrictHotSpots.DiskCompact.coordinates_injective line 159
  21. def OAI.StrictHotSpots.DiskCompact.regularizationParameter line 164
  22. lemma OAI.StrictHotSpots.DiskCompact.parameter_pos line 166
  23. lemma OAI.StrictHotSpots.DiskCompact.parameter_le_one line 169
  24. lemma OAI.StrictHotSpots.DiskCompact.parameter_tendsto line 172
  25. lemma OAI.StrictHotSpots.DiskCompact.parameter_tendsto_gt line 174
  26. def OAI.StrictHotSpots.DiskCompact.regularized line 177
  27. lemma OAI.StrictHotSpots.DiskCompact.regularized_pos line 194
  28. lemma OAI.StrictHotSpots.DiskCompact.regularized_symm line 197
  29. lemma OAI.StrictHotSpots.DiskCompact.regularized_onePositiveSquare line 200
  30. lemma OAI.StrictHotSpots.DiskCompact.regularized_tendsto_off line 206
  31. lemma OAI.StrictHotSpots.DiskCompact.regularized_tendsto_diagonal line 213
  32. lemma OAI.StrictHotSpots.DiskCompact.regularized_le line 218
  33. lemma OAI.StrictHotSpots.DiskCompact.preserving line 226
  34. lemma OAI.StrictHotSpots.DiskCompact.kernel_memLp line 232
  35. lemma OAI.StrictHotSpots.DiskCompact.ae_ne line 238
  36. def OAI.StrictHotSpots.DiskCompact.operator line 245
  37. lemma OAI.StrictHotSpots.DiskCompact.operator_ae line 250
  38. lemma OAI.StrictHotSpots.DiskCompact.operator_norm_le line 257
  39. theorem OAI.StrictHotSpots.DiskCompact.reciprocal line 266
  40. lemma OAI.StrictHotSpots.PlaneGreen.column_memLp line 305
  41. def OAI.StrictHotSpots.PlaneGreen.row line 310
  42. def OAI.StrictHotSpots.PlaneGreen.resolved line 312
  43. lemma OAI.StrictHotSpots.DiskCompact.observe_row line 324
  44. lemma OAI.StrictHotSpots.DiskCompact.resolved_eq line 329
  45. theorem OAI.StrictHotSpots.DiskCompact.reciprocal_ambient line 344
  46. lemma OAI.StrictHotSpots.DiskCompact.reciprocal_ambient_of_map line 354
  47. theorem OAI.StrictHotSpots.PlaneGreen.reciprocal_compact_support line 379
  48. lemma OAI.StrictHotSpots.DiskFormula.poisson_memLp_ae line 420
  49. lemma OAI.StrictHotSpots.DiskFormula.radial_one_memLp_ae line 431
  50. theorem OAI.StrictHotSpots.DiskFormula.radial_one_L2_ae line 445
  51. lemma OAI.StrictHotSpots.BanachResolvent.symmetric line 474
  52. lemma OAI.StrictHotSpots.L2Limits.inner_nonneg line 490
  53. lemma OAI.StrictHotSpots.PlaneGreen.kernel_nonneg line 500
  54. lemma OAI.StrictHotSpots.PlaneGreen.ae_mem_disk line 511
  55. lemma OAI.StrictHotSpots.PlaneGreen.row_nonneg line 515
  56. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_order_nonneg line 521
  57. lemma OAI.StrictHotSpots.PlaneGreen.resolved_ge line 530
  58. lemma OAI.StrictHotSpots.PlaneGreen.resolved_symm line 537
  59. abbrev OAI.StrictHotSpots.PlaneGreen.Boundary line 558
  60. def OAI.StrictHotSpots.PlaneGreen.poisson line 560
  61. def OAI.StrictHotSpots.PlaneGreen.boundaryInteraction line 563
  62. def OAI.StrictHotSpots.PlaneGreen.radial line 566
  63. lemma OAI.StrictHotSpots.PlaneGreen.poisson_nonneg line 570
  64. lemma OAI.StrictHotSpots.PlaneGreen.poisson_pos line 573
  65. lemma OAI.StrictHotSpots.PlaneGreen.boundaryInteraction_pos line 587
  66. lemma OAI.StrictHotSpots.PlaneGreen.poisson_memLp line 598
  67. def OAI.StrictHotSpots.PlaneGreen.poissonRow line 602
  68. lemma OAI.StrictHotSpots.PlaneGreen.poissonRow_nonneg line 604
  69. def OAI.StrictHotSpots.PlaneGreen.boundaryK line 612
  70. def OAI.StrictHotSpots.PlaneGreen.boundaryN line 616
  71. lemma OAI.StrictHotSpots.PlaneGreen.boundaryK_pos line 620
  72. lemma OAI.StrictHotSpots.PlaneGreen.boundaryN_pos line 627
  73. lemma OAI.StrictHotSpots.PlaneGreen.scaled_row_eq line 634
  74. lemma OAI.StrictHotSpots.PlaneGreen.scaled_row_tendsto line 654
  75. lemma OAI.StrictHotSpots.PlaneGreen.resolved_radial_one_eq line 667
  76. lemma OAI.StrictHotSpots.PlaneGreen.resolved_radial_two_eq line 675
  77. lemma OAI.StrictHotSpots.PlaneGreen.resolved_radial_one_tendsto line 685
  78. lemma OAI.StrictHotSpots.PlaneGreen.resolved_radial_two_tendsto line 708
  79. lemma OAI.StrictHotSpots.PlaneGreen.radial_injective line 744
  80. lemma OAI.StrictHotSpots.PlaneGreen.radial_ne_anchor line 751
  81. theorem OAI.StrictHotSpots.PlaneGreen.boundary_reciprocal_compact_support line 761
  82. def OAI.StrictHotSpots.PlaneGreen.distanceKernel line 833
  83. theorem OAI.StrictHotSpots.PlaneGreen.negative_kernel_compact_support line 837
  84. lemma OAI.StrictHotSpots.GreenLp.shifted_logPole_norm_bound_three line 868
  85. lemma OAI.StrictHotSpots.GreenLp.invnorm_memLp_three_halves line 890
  86. lemma OAI.StrictHotSpots.GreenLp.shifted_invnorm_memLp_bound line 903
  87. lemma OAI.StrictHotSpots.DiskFormula.green_uniform_L3_bound line 930
  88. lemma OAI.StrictHotSpots.DiskFormula.poisson_invnorm_bound line 951
  89. lemma OAI.StrictHotSpots.DiskFormula.poisson_memLp_three_halves line 968
  90. lemma OAI.StrictHotSpots.DiskFormula.poisson_uniform_L32_bound line 980
  91. lemma OAI.StrictHotSpots.PlaneGreen.kernel_memLp_three line 1013
  92. lemma OAI.StrictHotSpots.PlaneGreen.poisson_memLp_three_halves line 1018
  93. lemma OAI.StrictHotSpots.PlaneGreen.kernel_uniform_three_bound line 1023
  94. lemma OAI.StrictHotSpots.PlaneGreen.poisson_uniform_three_halves_bound line 1033
  95. lemma OAI.StrictHotSpots.PlaneGreen.kernel_memLp_three_weighted line 1047
  96. lemma OAI.StrictHotSpots.PlaneGreen.poisson_memLp_three_halves_weighted line 1051
  97. lemma OAI.StrictHotSpots.PlaneGreen.product_green_poisson_integrable line 1055
  98. lemma OAI.StrictHotSpots.PlaneGreen.kernel_uniform_three_bound_weighted line 1061
  99. lemma OAI.StrictHotSpots.PlaneGreen.poisson_uniform_three_halves_bound_weighted line 1070
  100. lemma OAI.StrictHotSpots.PlaneGreen.green_poisson_uniform_bound line 1079
  101. def OAI.StrictHotSpots.PlaneGreen.smoothedPoisson line 1097
  102. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_measurable line 1101
  103. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_memLp line 1107