OAI/Analysis/HotSpots/DouglasEnergy.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictHotSpots.Douglas.circleDatum line 18
  2. lemma OAI.StrictHotSpots.Douglas.circleDatum_toCircle line 24
  3. lemma OAI.StrictHotSpots.Douglas.circleDatum_circleMap line 37
  4. lemma OAI.StrictHotSpots.Douglas.circleDatum_circleIntegrable line 41
  5. lemma OAI.StrictHotSpots.Douglas.poisson_angle_continuous line 47
  6. lemma OAI.StrictHotSpots.Douglas.poissonExtension_eq_circleAverage line 55
  7. lemma OAI.StrictHotSpots.Douglas.poissonExtension_re_eq_circleAverage line 63
  8. lemma OAI.StrictHotSpots.Douglas.circleDatum_re_circleIntegrable line 78
  9. theorem OAI.StrictHotSpots.Douglas.poissonExtension_re_harmonic line 86
  10. lemma OAI.StrictHotSpots.Douglas.poissonExtension_re_contDiffOn line 95
  11. def OAI.StrictHotSpots.Douglas.planePoisson line 103
  12. lemma OAI.StrictHotSpots.Douglas.planePoisson_contDiffOn line 106
  13. lemma OAI.StrictHotSpots.Douglas.planePoisson_harmonic line 112
  14. lemma OAI.StrictHotSpots.Douglas.poisson_angle_kernel_nonneg line 133
  15. lemma OAI.StrictHotSpots.Douglas.poisson_angle_kernel_continuous line 141
  16. lemma OAI.StrictHotSpots.Douglas.poisson_angle_mass line 146
  17. theorem OAI.StrictHotSpots.Douglas.poissonExtension_norm_le line 155
  18. lemma OAI.StrictHotSpots.Douglas.planePoisson_norm_le line 173
  19. lemma OAI.StrictHotSpots.Douglas.planePoisson_memLp line 179
  20. lemma OAI.StrictHotSpots.Douglas.circleSmooth_sup_norm_le line 187
  21. theorem OAI.StrictHotSpots.Douglas.circleSmooth_planePoisson_tendsto_L2 line 193
  22. lemma OAI.StrictHotSpots.Douglas.poissonExtension_sub line 224
  23. lemma OAI.StrictHotSpots.Douglas.planePoisson_sub line 233
  24. lemma OAI.StrictHotSpots.Douglas.planePoisson_eq_series line 239
  25. lemma OAI.StrictHotSpots.Douglas.smooth_planePoisson_hasH1Gradient line 248
  26. def OAI.StrictHotSpots.Douglas.smoothPoissonH1 line 262
  27. lemma OAI.StrictHotSpots.Douglas.smoothPoissonH1_value line 266
  28. lemma OAI.StrictHotSpots.Douglas.smoothPoissonH1_sub line 270
  29. lemma OAI.StrictHotSpots.Douglas.lp_norm_sq_eq_integral_norm_sq line 284
  30. lemma OAI.StrictHotSpots.Douglas.norm_toLp_sq_eq_integral_norm_sq line 290
  31. lemma OAI.StrictHotSpots.Douglas.smoothPoissonH1_grad_energy_le line 299
  32. theorem OAI.StrictHotSpots.HasH1Gradient.eq_gradient_of_contDiffOn line 341
  33. lemma OAI.StrictHotSpots.HasH1Gradient.actual_of_contDiffOn line 389
  34. lemma OAI.StrictHotSpots.Douglas.cauchySeq_of_pair_norm_sq_zero line 408
  35. theorem OAI.StrictHotSpots.Douglas.circleSmooth_cauchy_H1 line 425
  36. theorem OAI.StrictHotSpots.Douglas.hasH1Gradient_of_circleSmooth line 455
  37. def OAI.StrictHotSpots.Douglas.circleApproxBump line 473
  38. lemma OAI.StrictHotSpots.Douglas.circleApproxBump_rOut_tendsto line 481
  39. theorem OAI.StrictHotSpots.Douglas.lipschitz_planePoisson_hasH1Gradient line 486
  40. theorem OAI.StrictHotSpots.Douglas.circleSmooth_tendsto_H1 line 506
  41. def OAI.StrictHotSpots.Douglas.poissonRealEnergy line 521
  42. lemma OAI.StrictHotSpots.Douglas.smoothPoissonH1_grad_norm_sq line 524
  43. lemma OAI.StrictHotSpots.Douglas.lipschitzPoissonH1_grad_norm_sq line 529
  44. lemma OAI.StrictHotSpots.Douglas.circleSmooth_realEnergy_tendsto line 534
  45. lemma OAI.StrictHotSpots.Douglas.poissonExtension_smul line 545
  46. lemma OAI.StrictHotSpots.Douglas.circleSmooth_smul line 552
  47. def OAI.StrictHotSpots.Douglas.imagDatum line 563
  48. lemma OAI.StrictHotSpots.Douglas.imagDatum_chordLipschitz line 565
  49. lemma OAI.StrictHotSpots.Douglas.planePoisson_imagDatum line 571
  50. lemma OAI.StrictHotSpots.Douglas.circleSmooth_imagDatum line 578
  51. lemma OAI.StrictHotSpots.Douglas.poissonExtension_im_eq line 582
  52. lemma OAI.StrictHotSpots.Douglas.poissonExtension_contDiffOn line 588
  53. lemma OAI.StrictHotSpots.Douglas.planeGradient_norm_sq line 612
  54. lemma OAI.StrictHotSpots.Douglas.planePoisson_fderiv line 627
  55. lemma OAI.StrictHotSpots.Douglas.planePoisson_im_fderiv line 640
  56. lemma OAI.StrictHotSpots.Douglas.poisson_energy_pointwise line 657
  57. theorem OAI.StrictHotSpots.Douglas.poisson_energy_components line 669
  58. theorem OAI.StrictHotSpots.Douglas.douglas_lipschitz line 693
  59. lemma OAI.StrictHotSpots.Douglas.chordLipschitz_equicontinuous line 723
  60. lemma OAI.StrictHotSpots.Douglas.circleSmooth_tendsto_uniform line 741
  61. def OAI.StrictHotSpots.Douglas.closedPoisson line 755
  62. lemma OAI.StrictHotSpots.Douglas.closedPoisson_interior line 759
  63. lemma OAI.StrictHotSpots.Douglas.closedPoisson_boundary line 764
  64. lemma OAI.StrictHotSpots.Douglas.exists_toCircle line 769
  65. lemma OAI.StrictHotSpots.Douglas.smooth_closedPoisson_continuousOn line 776
  66. lemma OAI.StrictHotSpots.Douglas.closedPoisson_sub line 791
  67. lemma OAI.StrictHotSpots.Douglas.closedPoisson_norm_le line 800
  68. theorem OAI.StrictHotSpots.Douglas.closedPoisson_continuousOn line 813
  69. lemma OAI.StrictHotSpots.Douglas.poissonExtension_im_zero line 845
  70. lemma OAI.StrictHotSpots.Douglas.poissonRealEnergy_imag_zero line 854
  71. theorem OAI.StrictHotSpots.Douglas.douglas_lipschitz_real line 872
  72. lemma OAI.StrictHotSpots.Douglas.lipschitzPoissonH1_sub line 879
  73. lemma OAI.StrictHotSpots.Douglas.boundaryDifference_sub line 894
  74. def OAI.StrictHotSpots.Douglas.boundaryRealCross line 899
  75. lemma OAI.StrictHotSpots.Douglas.boundaryRealCross_integrable line 902
  76. lemma OAI.StrictHotSpots.Douglas.boundaryEnergy_sub line 912
  77. lemma OAI.StrictHotSpots.Douglas.lipschitzPoisson_grad_sub_norm_sq line 928
  78. lemma OAI.StrictHotSpots.Douglas.inner_eq_of_polarization line 935
  79. lemma OAI.StrictHotSpots.Douglas.lipschitzPoisson_grad_norm_sq_real line 942
  80. lemma OAI.StrictHotSpots.Douglas.lipschitzPoisson_grad_sub_norm_sq_real line 947
  81. theorem OAI.StrictHotSpots.Douglas.douglas_lipschitz_bilinear line 961
  82. lemma OAI.StrictHotSpots.Douglas.lipschitzPoisson_weak_harmonic line 988
  83. def OAI.StrictHotSpots.Douglas.closedPlanePoisson line 1000
  84. lemma OAI.StrictHotSpots.Douglas.closedPlanePoisson_eqOn line 1003
  85. lemma OAI.StrictHotSpots.Douglas.closedPlanePoisson_boundary line 1009
  86. lemma OAI.StrictHotSpots.Douglas.closedPlanePoisson_contDiffOn line 1013
  87. lemma OAI.StrictHotSpots.Douglas.closedPlanePoisson_continuousOn line 1017
  88. lemma OAI.StrictHotSpots.Douglas.closedPlanePoisson_hasH1Gradient line 1026
  89. lemma OAI.StrictHotSpots.Douglas.closedPlanePoisson_toH1 line 1035
  90. theorem OAI.StrictHotSpots.Douglas.lipschitzPoisson_boundary_class line 1051
  91. theorem OAI.StrictHotSpots.Douglas.lipschitzPoisson_eq_harmonicLift line 1090