OAI/Analysis/HotSpots/BoundaryEnergy.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.SubcriticalExtension.energy_cancel line 15
  2. lemma OAI.StrictHotSpots.SubcriticalExtension.extension_energy line 30
  3. def OAI.StrictHotSpots.SubcriticalExtension.WeakPotential line 88
  4. lemma OAI.StrictHotSpots.SubcriticalExtension.weakPotential_sub line 92
  5. lemma OAI.StrictHotSpots.SubcriticalExtension.weakPotential_zero_class line 111
  6. lemma OAI.StrictHotSpots.SubcriticalExtension.extension_difference line 122
  7. lemma OAI.StrictHotSpots.SubcriticalExtension.weakPotential_unique line 130
  8. theorem OAI.StrictHotSpots.SubcriticalExtension.existsUnique_weakPotential line 148
  9. def OAI.StrictHotSpots.PlaneGreen.circleBoundary line 184
  10. def OAI.StrictHotSpots.PlaneGreen.angleBoundary line 192
  11. def OAI.StrictHotSpots.PlaneGreen.boundaryMeasure line 196
  12. instance OAI.StrictHotSpots.PlaneGreen.boundaryMeasure_finite line 198
  13. instance OAI.StrictHotSpots.PlaneGreen.boundaryMeasure_nullSingleton line 202
  14. instance OAI.StrictHotSpots.PlaneGreen.boundaryMeasure_openPos line 210
  15. lemma OAI.StrictHotSpots.PlaneGreen.boundaryMeasure_univ line 213
  16. lemma OAI.StrictHotSpots.PlaneGreen.boundaryMeasure_real line 217
  17. lemma OAI.StrictHotSpots.PlaneGreen.integral_boundary_angles line 220
  18. lemma OAI.StrictHotSpots.PlaneGreen.poisson_eq_standard line 231
  19. lemma OAI.StrictHotSpots.PlaneGreen.integral_poisson line 238
  20. lemma OAI.StrictHotSpots.PlaneGreen.poisson_continuous_boundary line 272
  21. lemma OAI.StrictHotSpots.PlaneGreen.poisson_joint_measurable line 286
  22. lemma OAI.StrictHotSpots.PlaneGreen.poissonRow_continuous line 293
  23. lemma OAI.StrictHotSpots.PlaneGreen.smoothedRow_stronglyMeasurable line 310
  24. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_joint_measurable line 330
  25. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryK_measurable line 347
  26. lemma OAI.StrictHotSpots.PlaneGreen.boundaryInteraction_measurable line 361
  27. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryN_measurable line 366
  28. instance OAI.StrictHotSpots.PlaneGreen.boundary_compactSpace line 403
  29. lemma OAI.StrictHotSpots.PlaneGreen.poisson_boundary_integrable line 405
  30. lemma OAI.StrictHotSpots.PlaneGreen.poisson_integrable_weighted line 413
  31. lemma OAI.StrictHotSpots.PlaneGreen.poisson_product_boundary_integrable line 419
  32. lemma OAI.StrictHotSpots.PlaneGreen.firstInteraction_integrable line 437
  33. lemma OAI.StrictHotSpots.PlaneGreen.integral_firstInteraction line 442
  34. def OAI.StrictHotSpots.PlaneGreen.poissonExtension line 450
  35. lemma OAI.StrictHotSpots.PlaneGreen.poissonExtension_norm_le line 453
  36. lemma OAI.StrictHotSpots.L2Rows.integral_eq_toLp line 483
  37. lemma OAI.StrictHotSpots.L2Rows.average_memLp line 506
  38. lemma OAI.StrictHotSpots.L2Rows.integrable_pair_of_bound line 519
  39. lemma OAI.StrictHotSpots.L2Rows.integral_eq_toLp_of_bound line 531
  40. lemma OAI.StrictHotSpots.PlaneGreen.poissonExtension_measurable line 550
  41. lemma OAI.StrictHotSpots.PlaneGreen.poissonExtension_memLp line 557
  42. def OAI.StrictHotSpots.PlaneGreen.poissonL2 line 565
  43. lemma OAI.StrictHotSpots.PlaneGreen.smoothedRow_uniform_bound line 569
  44. lemma OAI.StrictHotSpots.PlaneGreen.smoothedRow_integrable line 577
  45. lemma OAI.StrictHotSpots.PlaneGreen.green_poisson_boundary_integrable line 589
  46. lemma OAI.StrictHotSpots.PlaneGreen.green_poisson_data_integrable line 605
  47. lemma OAI.StrictHotSpots.PlaneGreen.smoothedPoisson_average line 618
  48. lemma OAI.StrictHotSpots.PlaneGreen.smoothedRow_average line 635
  49. lemma OAI.StrictHotSpots.PlaneGreen.inner_row line 679
  50. lemma OAI.StrictHotSpots.PlaneGreen.inner_row_poissonL2 line 687
  51. def OAI.StrictHotSpots.PlaneGreen.fullExtension line 697
  52. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryK_data_integrable line 701
  53. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryK_representation line 712
  54. lemma OAI.StrictHotSpots.PlaneGreen.poisson_pair_integrable line 776
  55. lemma OAI.StrictHotSpots.PlaneGreen.poisson_data_pair_integrable line 791
  56. lemma OAI.StrictHotSpots.PlaneGreen.poisson_average_pairing line 803
  57. lemma OAI.StrictHotSpots.PlaneGreen.poissonL2_pairing line 824
  58. def OAI.StrictHotSpots.PlaneGreen.firstInteraction line 844
  59. def OAI.StrictHotSpots.PlaneGreen.secondInteraction line 846
  60. def OAI.StrictHotSpots.PlaneGreen.tailInteraction line 848
  61. def OAI.StrictHotSpots.PlaneGreen.fullBoundaryR line 851
  62. lemma OAI.StrictHotSpots.PlaneGreen.firstInteraction_measurable line 854
  63. lemma OAI.StrictHotSpots.PlaneGreen.secondInteraction_measurable line 862
  64. lemma OAI.StrictHotSpots.PlaneGreen.tailInteraction_measurable line 870
  65. lemma OAI.StrictHotSpots.PlaneGreen.firstInteraction_nonneg line 879
  66. lemma OAI.StrictHotSpots.PlaneGreen.secondInteraction_nonneg line 886
  67. lemma OAI.StrictHotSpots.PlaneGreen.tailInteraction_nonneg line 891
  68. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryR_nonneg line 896
  69. lemma OAI.StrictHotSpots.PlaneGreen.massPoisson_integrable line 902
  70. lemma OAI.StrictHotSpots.PlaneGreen.firstInteraction_prod_integrable line 907
  71. lemma OAI.StrictHotSpots.PlaneGreen.secondInteraction_bound line 919
  72. lemma OAI.StrictHotSpots.PlaneGreen.secondInteraction_prod_integrable line 935
  73. lemma OAI.StrictHotSpots.PlaneGreen.tailInteraction_prod_integrable line 942
  74. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryR_integrable line 953
  75. lemma OAI.StrictHotSpots.PlaneGreen.firstInteraction_average line 970
  76. lemma OAI.StrictHotSpots.PlaneGreen.firstInteraction_pairing line 988
  77. lemma OAI.StrictHotSpots.PlaneGreen.smoothed_average_ae line 1001
  78. lemma OAI.StrictHotSpots.PlaneGreen.smoothed_data_pair_integrable line 1011
  79. lemma OAI.StrictHotSpots.PlaneGreen.smoothed_average_pairing line 1028
  80. lemma OAI.StrictHotSpots.PlaneGreen.secondInteraction_average line 1047
  81. lemma OAI.StrictHotSpots.PlaneGreen.secondInteraction_pairing line 1056
  82. lemma OAI.StrictHotSpots.PlaneGreen.tailInteraction_pairing line 1063
  83. lemma OAI.StrictHotSpots.PlaneGreen.boundary_data_integrable line 1105
  84. lemma OAI.StrictHotSpots.PlaneGreen.interaction_eq_iterated line 1118
  85. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryR_representation line 1135
  86. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryN_eq line 1166
  87. lemma OAI.StrictHotSpots.PlaneGreen.boundaryInteraction_symm line 1182
  88. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryN_symm line 1185
  89. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryR_symm line 1201
  90. lemma OAI.StrictHotSpots.PlaneGreen.poissonL2_one_ae line 1207
  91. lemma OAI.StrictHotSpots.PlaneGreen.poissonL2_one_norm_sq line 1215
  92. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryR_integral_le line 1227
  93. lemma OAI.StrictHotSpots.PlaneGreen.boundary_continuous_bound line 1258
  94. lemma OAI.StrictHotSpots.PlaneGreen.harmonic_boundary_bound line 1263
  95. lemma OAI.StrictHotSpots.PlaneGreen.harmonic_boundary_integrable line 1277
  96. lemma OAI.StrictHotSpots.PlaneGreen.interaction_boundary_integrable line 1287
  97. lemma OAI.StrictHotSpots.PlaneGreen.curvature_boundary_integrable line 1306
  98. def OAI.StrictHotSpots.PlaneGreen.boundaryForm line 1323
  99. lemma OAI.StrictHotSpots.PlaneGreen.harmonic_multiplier_algebra line 1329
  100. lemma OAI.StrictHotSpots.PlaneGreen.boundary_smul_lipschitz line 1336