OAI/Analysis/HotSpots/Green.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictHotSpots.GreenFundamental.logRegularized line 21
  2. def OAI.StrictHotSpots.GreenFundamental.peak line 23
  3. lemma OAI.StrictHotSpots.GreenFundamental.denominator_pos line 25
  4. lemma OAI.StrictHotSpots.GreenFundamental.logRegularized_contDiff line 28
  5. lemma OAI.StrictHotSpots.GreenFundamental.logRegularized_fderiv line 33
  6. lemma OAI.StrictHotSpots.GreenFundamental.logRegularized_second line 39
  7. lemma OAI.StrictHotSpots.GreenFundamental.logRegularized_laplacian line 60
  8. lemma OAI.StrictHotSpots.GreenFundamental.radial_primitive_hasDerivAt line 72
  9. lemma OAI.StrictHotSpots.GreenFundamental.radial_primitive_tendsto line 83
  10. lemma OAI.StrictHotSpots.GreenFundamental.integral_radial line 89
  11. lemma OAI.StrictHotSpots.GreenFundamental.integral_peak line 95
  12. lemma OAI.StrictHotSpots.GreenFundamental.peak_nonneg line 111
  13. lemma OAI.StrictHotSpots.GreenFundamental.peak_decay line 115
  14. lemma OAI.StrictHotSpots.GreenFundamental.tendsto_peak_mul line 128
  15. lemma OAI.StrictHotSpots.GreenFundamental.logRegularized_laplacian_scale line 134
  16. lemma OAI.StrictHotSpots.GreenFundamental.tendsto_logRegularized_laplacian_mul line 143
  17. def OAI.StrictHotSpots.GreenFundamental.direction line 153
  18. lemma OAI.StrictHotSpots.GreenFundamental.direction_smooth line 155
  19. lemma OAI.StrictHotSpots.GreenFundamental.direction_compact line 159
  20. lemma OAI.StrictHotSpots.GreenFundamental.second_direction line 162
  21. lemma OAI.StrictHotSpots.GreenFundamental.laplacian_direction line 169
  22. lemma OAI.StrictHotSpots.GreenFundamental.integral_direction_by_parts line 177
  23. lemma OAI.StrictHotSpots.GreenFundamental.integral_second_direction line 191
  24. lemma OAI.StrictHotSpots.GreenFundamental.integral_laplacian_by_parts line 198
  25. lemma OAI.StrictHotSpots.GreenFundamental.tendsto_logRegularized_test line 209
  26. lemma OAI.StrictHotSpots.GreenFundamental.abs_log_bound line 218
  27. lemma OAI.StrictHotSpots.GreenFundamental.log_norm_integrableOn_ball line 223
  28. lemma OAI.StrictHotSpots.GreenFundamental.logRegularized_abs_le line 243
  29. lemma OAI.StrictHotSpots.GreenFundamental.tendsto_logRegularized line 256
  30. lemma OAI.StrictHotSpots.GreenFundamental.tendsto_integral_logRegularized line 263
  31. lemma OAI.StrictHotSpots.GreenFundamental.laplacian_smooth line 298
  32. lemma OAI.StrictHotSpots.GreenFundamental.laplacian_compact line 304
  33. lemma OAI.StrictHotSpots.GreenFundamental.integral_log_laplacian line 312
  34. lemma OAI.StrictHotSpots.GreenFundamental.log_norm_locallyIntegrable line 322
  35. lemma OAI.StrictHotSpots.GreenFundamental.laplacian_comp_add_right line 328
  36. lemma OAI.StrictHotSpots.GreenFundamental.integral_log_sub_laplacian line 333
  37. lemma OAI.StrictHotSpots.GreenFundamental.integral_laplacian_zero line 343
  38. lemma OAI.StrictHotSpots.GreenFundamental.log_sub_mul_integrable line 347
  39. def OAI.StrictHotSpots.DiskFormula.green line 363
  40. lemma OAI.StrictHotSpots.DiskFormula.disk_cross_identity line 366
  41. lemma OAI.StrictHotSpots.DiskFormula.green_eq_log line 373
  42. lemma OAI.StrictHotSpots.DiskFormula.correction_factor line 384
  43. lemma OAI.StrictHotSpots.DiskFormula.ae_correction_ne_zero line 390
  44. lemma OAI.StrictHotSpots.DiskFormula.log_correction_eq line 397
  45. lemma OAI.StrictHotSpots.DiskFormula.log_correction_mul_integrable line 402
  46. lemma OAI.StrictHotSpots.DiskFormula.integral_log_correction_laplacian line 414
  47. lemma OAI.StrictHotSpots.DiskFormula.integral_green_laplacian line 440
  48. lemma OAI.StrictHotSpots.GreenPotential.direction_convolution line 463
  49. lemma OAI.StrictHotSpots.GreenPotential.laplacian_convolution line 472
  50. lemma OAI.StrictHotSpots.GreenPotential.log_potential_smooth line 489
  51. lemma OAI.StrictHotSpots.GreenPotential.laplacian_comp_neg line 494
  52. lemma OAI.StrictHotSpots.GreenPotential.laplacian_comp_const_sub line 503
  53. lemma OAI.StrictHotSpots.GreenPotential.log_potential_laplacian line 518
  54. def OAI.StrictHotSpots.GreenPotential.correctionIntegrand line 531
  55. lemma OAI.StrictHotSpots.GreenPotential.correctionIntegrand_contDiffOn line 534
  56. lemma OAI.StrictHotSpots.GreenPotential.correction_potential_smooth line 553
  57. lemma OAI.StrictHotSpots.CompactParameter.fderiv_eq_zero_outside line 577
  58. lemma OAI.StrictHotSpots.CompactParameter.fderiv_section_compact line 586
  59. lemma OAI.StrictHotSpots.CompactParameter.fderiv_section_continuous line 593
  60. lemma OAI.StrictHotSpots.CompactParameter.hasFDerivAt_integral line 599
  61. def OAI.StrictHotSpots.CompactParameter.paramDeriv line 636
  62. lemma OAI.StrictHotSpots.CompactParameter.partial_contDiffOn line 639
  63. lemma OAI.StrictHotSpots.CompactParameter.partial_zero_outside line 643
  64. lemma OAI.StrictHotSpots.CompactParameter.integral_contDiffOn line 649
  65. lemma OAI.StrictHotSpots.CompactParameter.fderiv_integral_apply line 662
  66. lemma OAI.StrictHotSpots.CompactParameter.fderiv_section_apply line 673
  67. lemma OAI.StrictHotSpots.CompactParameter.second_integral_apply line 683
  68. lemma OAI.StrictHotSpots.CompactParameter.second_section_apply line 696
  69. lemma OAI.StrictHotSpots.CompactParameter.integrable_section line 707
  70. lemma OAI.StrictHotSpots.CompactParameter.laplacian_directions_at line 716
  71. lemma OAI.StrictHotSpots.CompactParameter.laplacian_integral line 728
  72. lemma OAI.StrictHotSpots.GreenPotential.correction_potential_laplacian line 756
  73. lemma OAI.StrictHotSpots.GreenPotential.log_potential_eq line 775
  74. def OAI.StrictHotSpots.GreenPotential.potential line 785
  75. lemma OAI.StrictHotSpots.GreenPotential.potential_contDiffOn line 789
  76. lemma OAI.StrictHotSpots.GreenPotential.potential_laplacian line 796
  77. lemma OAI.StrictHotSpots.GreenPotential.potential_eq_zero_on_circle line 821
  78. lemma OAI.StrictHotSpots.GreenPotential.potential_eq_integral line 829
  79. lemma OAI.StrictHotSpots.GreenPotential.exists_regular_neighborhood line 849
  80. lemma OAI.StrictHotSpots.GreenPotential.potential_smooth_near_closed_disk line 870
  81. lemma OAI.StrictHotSpots.laplacian_comp_linearIsometryEquiv line 887
  82. lemma OAI.StrictHotSpots.PlaneGreen.diskOpen line 913
  83. def OAI.StrictHotSpots.PlaneGreen.complexIso line 915
  84. def OAI.StrictHotSpots.PlaneGreen.source line 917
  85. def OAI.StrictHotSpots.PlaneGreen.potential line 919
  86. lemma OAI.StrictHotSpots.PlaneGreen.source_contDiff line 922
  87. lemma OAI.StrictHotSpots.PlaneGreen.source_compact line 926
  88. lemma OAI.StrictHotSpots.PlaneGreen.source_support line 930
  89. lemma OAI.StrictHotSpots.PlaneGreen.smooth_near_closed_disk line 937
  90. lemma OAI.StrictHotSpots.PlaneGreen.zero_on_circle line 952
  91. lemma OAI.StrictHotSpots.PlaneGreen.value_mk line 956
  92. lemma OAI.StrictHotSpots.PlaneGreen.grad_mk line 959
  93. lemma OAI.StrictHotSpots.PlaneGreen.energy_mk line 962
  94. lemma OAI.StrictHotSpots.PlaneGreen.exists_smooth_weak_solution line 965
  95. lemma OAI.StrictHotSpots.PlaneGreen.exists_dirichlet_representative line 985