OAI/Analysis/HotSpots/GreenOperator.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictHotSpots.DiskFormula.poisson line 26
  2. def OAI.StrictHotSpots.DiskFormula.boundaryInteraction line 28
  3. def OAI.StrictHotSpots.DiskFormula.logRatio line 30
  4. lemma OAI.StrictHotSpots.DiskFormula.logRatio_zero line 32
  5. lemma OAI.StrictHotSpots.DiskFormula.logRatio_continuousAt_zero line 35
  6. lemma OAI.StrictHotSpots.DiskFormula.log_eq_mul_ratio line 41
  7. lemma OAI.StrictHotSpots.DiskFormula.tendsto_log_mul_div line 45
  8. lemma OAI.StrictHotSpots.DiskFormula.radial_one_formula line 58
  9. lemma OAI.StrictHotSpots.DiskFormula.radial_one line 63
  10. lemma OAI.StrictHotSpots.DiskFormula.radial_two_formula line 99
  11. lemma OAI.StrictHotSpots.DiskFormula.radial_two line 105
  12. lemma OAI.StrictHotSpots.DiskFormula.log_mul_div_bounds line 147
  13. lemma OAI.StrictHotSpots.DiskFormula.radial_one_bounded line 156
  14. lemma OAI.StrictHotSpots.DiskFormula.poisson_nonneg line 196
  15. lemma OAI.StrictHotSpots.DiskFormula.poisson_bounded line 200
  16. lemma OAI.StrictHotSpots.DiskFormula.poisson_memLp line 215
  17. lemma OAI.StrictHotSpots.DiskFormula.radial_one_memLp line 226
  18. theorem OAI.StrictHotSpots.DiskFormula.radial_one_L2 line 240
  19. def OAI.StrictHotSpots.GreenLp.logPole line 269
  20. lemma OAI.StrictHotSpots.GreenLp.logPole_nonneg line 271
  21. lemma OAI.StrictHotSpots.GreenLp.measurable_logPole line 276
  22. lemma OAI.StrictHotSpots.GreenLp.logPole_cube_bound line 280
  23. lemma OAI.StrictHotSpots.GreenLp.logPole_cube_integrable line 308
  24. lemma OAI.StrictHotSpots.GreenLp.logPole_memLp_three line 320
  25. lemma OAI.StrictHotSpots.GreenLp.shifted_logPole_memLp_three line 326
  26. lemma OAI.StrictHotSpots.DiskFormula.measurable_green_left line 352
  27. lemma OAI.StrictHotSpots.DiskFormula.green_bounds line 356
  28. lemma OAI.StrictHotSpots.DiskFormula.green_pos line 370
  29. lemma OAI.StrictHotSpots.DiskFormula.green_memLp_three line 380
  30. lemma OAI.StrictHotSpots.DiskFormula.green_memLp_two line 394
  31. lemma OAI.StrictHotSpots.DiskFormula.green_memLp_three_of_le line 400
  32. lemma OAI.StrictHotSpots.DiskFormula.green_memLp_two_of_le line 405
  33. lemma OAI.StrictHotSpots.GreenLp.logPole_memLp_two line 417
  34. lemma OAI.StrictHotSpots.GreenLp.shifted_logPole_norm_bound line 422
  35. lemma OAI.StrictHotSpots.DiskFormula.green_uniform_L2_bound line 448
  36. lemma OAI.StrictHotSpots.MeasurableL2Kernel.integral_mul_eq_inner line 478
  37. lemma OAI.StrictHotSpots.MeasurableL2Kernel.norm_integral_mul_le line 487
  38. lemma OAI.StrictHotSpots.MeasurableL2Kernel.apply_bound line 502
  39. lemma OAI.StrictHotSpots.MeasurableL2Kernel.apply_memLp line 511
  40. def OAI.StrictHotSpots.MeasurableL2Kernel.operator line 520
  41. lemma OAI.StrictHotSpots.MeasurableL2Kernel.operator_apply_ae line 564
  42. lemma OAI.StrictHotSpots.eq_zero_of_inner_smoothTest_eq_zero line 576
  43. lemma OAI.StrictHotSpots.smoothTest_dense_L2 line 599
  44. def OAI.StrictHotSpots.DirichletOperator.solution line 633
  45. lemma OAI.StrictHotSpots.DirichletOperator.solution_spec line 637
  46. def OAI.StrictHotSpots.DirichletOperator.green line 644
  47. lemma OAI.StrictHotSpots.DirichletOperator.green_apply line 647
  48. lemma OAI.StrictHotSpots.DirichletOperator.green_symmetric line 650
  49. lemma OAI.StrictHotSpots.DirichletOperator.green_nonneg line 659
  50. lemma OAI.StrictHotSpots.DirichletOperator.green_norm_le line 667
  51. lemma OAI.StrictHotSpots.DirichletOperator.green_norm_lt_one line 686
  52. lemma OAI.StrictHotSpots.PlaneGreen.diskBounded line 699
  53. instance OAI.StrictHotSpots.PlaneGreen.diskFinite line 701
  54. def OAI.StrictHotSpots.PlaneGreen.kernel line 704
  55. lemma OAI.StrictHotSpots.PlaneGreen.complexIso_disk_preserving line 706
  56. lemma OAI.StrictHotSpots.PlaneGreen.kernel_memLp line 715
  57. lemma OAI.StrictHotSpots.PlaneGreen.measurable_kernel line 720
  58. lemma OAI.StrictHotSpots.PlaneGreen.kernel_bound line 724
  59. lemma OAI.StrictHotSpots.PlaneGreen.kernel_rows line 736
  60. def OAI.StrictHotSpots.PlaneGreen.integralOperator line 740
  61. lemma OAI.StrictHotSpots.PlaneGreen.integralOperator_ae line 746
  62. lemma OAI.StrictHotSpots.PlaneGreen.potential_eq_integral line 750
  63. def OAI.StrictHotSpots.PlaneGreen.variationalOperator line 774
  64. lemma OAI.StrictHotSpots.PlaneGreen.variationalOperator_test line 780
  65. lemma OAI.StrictHotSpots.PlaneGreen.integralOperator_eq_variationalOperator line 801
  66. def OAI.StrictHotSpots.H10.weightedValue line 828
  67. lemma OAI.StrictHotSpots.H10.weightedValue_ae line 831
  68. def OAI.StrictHotSpots.H10.greenOperator line 837
  69. lemma OAI.StrictHotSpots.H10.energy_symmetric line 843
  70. lemma OAI.StrictHotSpots.H10.greenOperator_symmetric line 849
  71. lemma OAI.StrictHotSpots.H10.greenOperator_nonneg line 855
  72. lemma OAI.StrictHotSpots.H10.greenOperator_norm_le line 861
  73. lemma OAI.StrictHotSpots.DirichletOperator.green_comp line 876
  74. def OAI.StrictHotSpots.PlaneGreen.inclusion line 890
  75. lemma OAI.StrictHotSpots.PlaneGreen.inclusion_ae line 893
  76. lemma OAI.StrictHotSpots.PlaneGreen.kernel_memLp_weighted line 897
  77. lemma OAI.StrictHotSpots.PlaneGreen.inclusion_row line 900
  78. lemma OAI.StrictHotSpots.PlaneGreen.integral_adjoint_row line 908
  79. def OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator line 919
  80. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_ae line 922
  81. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_eq_greenOperator line 931
  82. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_norm_le line 940
  83. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_symmetric line 946
  84. lemma OAI.StrictHotSpots.PlaneGreen.weightedIntegralOperator_nonneg line 952