OAI/Analysis/HotSpots/Douglas.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.StrictHotSpots.Douglas.haar_nullSingleton line 15
  2. def OAI.StrictHotSpots.Douglas.polynomial line 25
  3. lemma OAI.StrictHotSpots.Douglas.polynomial_apply line 29
  4. lemma OAI.StrictHotSpots.Douglas.integral_norm_sq_polynomial line 33
  5. lemma OAI.StrictHotSpots.Douglas.fourier_nat line 59
  6. lemma OAI.StrictHotSpots.Douglas.polynomial_geom line 66
  7. lemma OAI.StrictHotSpots.Douglas.normalized_monomial_quotient line 74
  8. theorem OAI.StrictHotSpots.Douglas.monomial_double_integral line 95
  9. def OAI.StrictHotSpots.Douglas.boundaryDifference line 114
  10. def OAI.StrictHotSpots.Douglas.ChordLipschitz line 118
  11. lemma OAI.StrictHotSpots.Douglas.boundaryDifference_bound line 122
  12. lemma OAI.StrictHotSpots.Douglas.measurable_boundaryDifference line 131
  13. lemma OAI.StrictHotSpots.Douglas.integrable_boundaryDifference_sq line 138
  14. def OAI.StrictHotSpots.Douglas.boundaryEnergy line 148
  15. theorem OAI.StrictHotSpots.Douglas.boundaryEnergy_tendsto line 153
  16. lemma OAI.StrictHotSpots.Douglas.fourier_shift line 177
  17. def OAI.StrictHotSpots.Douglas.boundaryModeCross line 182
  18. lemma OAI.StrictHotSpots.Douglas.boundaryModeCross_shift line 187
  19. theorem OAI.StrictHotSpots.Douglas.boundaryModeCross_integral_zero line 198
  20. lemma OAI.StrictHotSpots.Douglas.integral_disk_norm_pow line 219
  21. lemma OAI.StrictHotSpots.Douglas.holomorphic_mode_energy line 265
  22. def OAI.StrictHotSpots.Douglas.harmonicMode line 284
  23. lemma OAI.StrictHotSpots.Douglas.harmonicMode_boundary line 288
  24. lemma OAI.StrictHotSpots.Douglas.harmonicMode_harmonic line 296
  25. lemma OAI.StrictHotSpots.Douglas.harmonicMode_continuous line 301
  26. lemma OAI.StrictHotSpots.Douglas.harmonicMode_poisson line 310
  27. lemma OAI.StrictHotSpots.Douglas.fderiv_pow_mode line 352
  28. lemma OAI.StrictHotSpots.Douglas.fderiv_conj_mode line 357
  29. theorem OAI.StrictHotSpots.Douglas.harmonicMode_energy line 369
  30. theorem OAI.StrictHotSpots.Douglas.fourier_double_integral line 398
  31. theorem OAI.StrictHotSpots.Douglas.douglas_for_mode line 415
  32. lemma OAI.StrictHotSpots.Douglas.norm_pow_sub_pow_of_unit line 433
  33. lemma OAI.StrictHotSpots.Douglas.chordLipschitz_fourier line 447
  34. lemma OAI.StrictHotSpots.Douglas.boundaryModeCross_eq line 460
  35. lemma OAI.StrictHotSpots.Douglas.integrable_boundaryModeCross line 466
  36. lemma OAI.StrictHotSpots.Douglas.boundaryDifference_sq_integral line 482
  37. theorem OAI.StrictHotSpots.Douglas.boundaryModeCross_integral line 499
  38. def OAI.StrictHotSpots.Douglas.boundaryPolynomial line 521
  39. lemma OAI.StrictHotSpots.Douglas.boundaryDifference_polynomial line 525
  40. lemma OAI.StrictHotSpots.Douglas.boundaryPolynomial_sq line 536
  41. lemma OAI.StrictHotSpots.Douglas.boundaryPolynomial_energy line 549
  42. def OAI.StrictHotSpots.Douglas.circleRotation line 592
  43. lemma OAI.StrictHotSpots.Douglas.circleRotation_apply line 601
  44. lemma OAI.StrictHotSpots.Douglas.integral_disk_rotation line 603
  45. lemma OAI.StrictHotSpots.Douglas.monomialCross_rotation line 626
  46. lemma OAI.StrictHotSpots.Douglas.integral_disk_monomial_cross_zero line 633
  47. lemma OAI.StrictHotSpots.Douglas.integrableOn_monomial_cross line 649
  48. lemma OAI.StrictHotSpots.Douglas.integral_disk_monomial_cross line 654
  49. def OAI.StrictHotSpots.Douglas.bulkModeCross line 673
  50. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_zero_left line 677
  51. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_symm line 681
  52. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_pos line 686
  53. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_neg line 698
  54. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_mixed line 714
  55. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_continuous line 725
  56. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_integrable line 767
  57. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_self_integral line 780
  58. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_pos_integral_zero line 790
  59. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_zero_right line 795
  60. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_opposite line 798
  61. lemma OAI.StrictHotSpots.Douglas.bulkModeCross_integral_zero line 802
  62. theorem OAI.StrictHotSpots.Douglas.bulkModeCross_integral line 837
  63. def OAI.StrictHotSpots.Douglas.harmonicPolynomial line 852
  64. lemma OAI.StrictHotSpots.Douglas.harmonicMode_differentiable line 855
  65. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_deriv line 861
  66. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_boundary line 870
  67. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_sq line 874
  68. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_energy line 889
  69. theorem OAI.StrictHotSpots.Douglas.douglas_polynomial line 924
  70. lemma OAI.StrictHotSpots.Douglas.harmonicMode_norm_le_one line 939
  71. lemma OAI.StrictHotSpots.Douglas.harmonicMode_deriv_apply_bound line 950
  72. lemma OAI.StrictHotSpots.Douglas.harmonicMode_deriv_bound line 975
  73. def OAI.StrictHotSpots.Douglas.harmonicSeries line 982
  74. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_summable line 984
  75. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_deriv_summable line 991
  76. def OAI.StrictHotSpots.Douglas.firstMoment line 1008
  77. lemma OAI.StrictHotSpots.Douglas.firstMoment_nonneg line 1009
  78. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_hasFDerivAt line 1012
  79. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_deriv_bound line 1028
  80. lemma OAI.StrictHotSpots.Douglas.harmonicMode_deriv_continuous line 1045
  81. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_deriv_continuous line 1062
  82. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_deriv_tendsto line 1067
  83. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_boundary_tendsto line 1089
  84. lemma OAI.StrictHotSpots.Douglas.boundaryPolynomial_chordLipschitz line 1099
  85. lemma OAI.StrictHotSpots.Douglas.boundaryPolynomial_continuous line 1117
  86. theorem OAI.StrictHotSpots.Douglas.boundaryEnergy_tendsto_filter line 1122
  87. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_boundaryEnergy_tendsto line 1136
  88. def OAI.StrictHotSpots.Douglas.diskEnergy line 1153
  89. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_diskEnergy_tendsto line 1156
  90. theorem OAI.StrictHotSpots.Douglas.douglas_series line 1184
  91. lemma OAI.StrictHotSpots.Douglas.poissonKernel_continuousOn_sphere line 1207
  92. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_continuous line 1222
  93. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_poisson line 1226
  94. lemma OAI.StrictHotSpots.Douglas.harmonicPolynomial_bound line 1249
  95. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_poisson_tendsto line 1262
  96. theorem OAI.StrictHotSpots.Douglas.harmonicSeries_poisson line 1293
  97. lemma OAI.StrictHotSpots.Douglas.norm_fourierCoeff_le line 1310
  98. lemma OAI.StrictHotSpots.Douglas.fourierCoeffOn_coe line 1321
  99. lemma OAI.StrictHotSpots.Douglas.fourierCoeff_derivative line 1328
  100. lemma OAI.StrictHotSpots.Douglas.norm_fourierCoeff_derivative line 1343
  101. lemma OAI.StrictHotSpots.Douglas.firstMoment_fourierCoeff_bound line 1352
  102. lemma OAI.StrictHotSpots.Douglas.summable_firstMoment_fourierCoeff line 1375
  103. lemma OAI.StrictHotSpots.Douglas.summable_norm_of_firstMoment line 1394
  104. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_fourier_boundary line 1403
  105. lemma OAI.StrictHotSpots.Douglas.circleMap_eq_toCircle line 1409
  106. def OAI.StrictHotSpots.Douglas.poissonExtension line 1418
  107. lemma OAI.StrictHotSpots.Douglas.poissonExtension_eq_harmonicSeries line 1421
  108. theorem OAI.StrictHotSpots.Douglas.douglas_C3 line 1434
  109. lemma OAI.StrictHotSpots.Douglas.harmonicMode_contDiff line 1464
  110. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_continuousOn line 1469
  111. def OAI.StrictHotSpots.Douglas.harmonicD line 1479
  112. lemma OAI.StrictHotSpots.Douglas.harmonicD_continuousOn line 1482
  113. lemma OAI.StrictHotSpots.Douglas.harmonicD_bound line 1494