OAI/Analysis/HotSpots/Helmholtz.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.PlaneWaves.cosine_h1_gradient line 14
  2. lemma OAI.StrictHotSpots.PlaneWaves.sine_h1_gradient line 16
  3. def OAI.StrictHotSpots.PlaneWaves.cosH1 line 19
  4. def OAI.StrictHotSpots.PlaneWaves.sinH1 line 20
  5. lemma OAI.StrictHotSpots.PlaneWaves.cosH1_pair line 22
  6. lemma OAI.StrictHotSpots.PlaneWaves.sinH1_pair line 41
  7. lemma OAI.StrictHotSpots.PlaneWaves.pair_sum line 60
  8. lemma OAI.StrictHotSpots.PlaneWaves.self_sum line 78
  9. lemma OAI.StrictHotSpots.PlaneWaves.cosH1_dirichlet_pair line 83
  10. lemma OAI.StrictHotSpots.PlaneWaves.sinH1_dirichlet_pair line 93
  11. def OAI.StrictHotSpots.LpZeroExtension.lift line 113
  12. lemma OAI.StrictHotSpots.LpZeroExtension.lift_ae line 117
  13. lemma OAI.StrictHotSpots.LpZeroExtension.lift_norm line 121
  14. def OAI.StrictHotSpots.LpZeroExtension.linearIsometry line 124
  15. lemma OAI.StrictHotSpots.LpZeroExtension.linearIsometry_ae line 146
  16. lemma OAI.StrictHotSpots.LpZeroExtension.linearIsometry_toLp line 149
  17. lemma OAI.StrictHotSpots.H10.inner_smul_reverse line 165
  18. def OAI.StrictHotSpots.H10.zeroValue line 171
  19. def OAI.StrictHotSpots.H10.zeroGrad line 174
  20. lemma OAI.StrictHotSpots.H10.zeroValue_test line 177
  21. lemma OAI.StrictHotSpots.H10.zeroGrad_test line 183
  22. lemma OAI.StrictHotSpots.H10.inner_zeroValue_toLp line 192
  23. lemma OAI.StrictHotSpots.H10.inner_zeroGrad_toLp line 199
  24. lemma OAI.StrictHotSpots.H10.zero_hasH1Gradient line 213
  25. lemma OAI.StrictHotSpots.Helmholtz.secondOrder_zero line 268
  26. lemma OAI.StrictHotSpots.Helmholtz.continuous_eq_zero_of_fourierCoeff line 302
  27. lemma OAI.StrictHotSpots.Helmholtz.bilinear_rotation line 314
  28. def OAI.StrictHotSpots.Helmholtz.direction line 335
  29. def OAI.StrictHotSpots.Helmholtz.radial line 337
  30. def OAI.StrictHotSpots.Helmholtz.radialDeriv line 338
  31. def OAI.StrictHotSpots.Helmholtz.radialSecond line 340
  32. def OAI.StrictHotSpots.Helmholtz.angularDeriv line 342
  33. def OAI.StrictHotSpots.Helmholtz.angularSecond line 344
  34. lemma OAI.StrictHotSpots.Helmholtz.point_eq line 348
  35. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_point_radius line 351
  36. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_radial line 356
  37. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_radialDeriv line 361
  38. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_angular line 370
  39. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_angularDeriv line 375
  40. lemma OAI.StrictHotSpots.Helmholtz.polar_laplacian line 385
  41. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_intervalIntegral_of_continuousOn line 413
  42. def OAI.StrictHotSpots.Helmholtz.weight line 452
  43. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_weight line 454
  44. lemma OAI.StrictHotSpots.Helmholtz.continuous_weight line 462
  45. lemma OAI.StrictHotSpots.Helmholtz.weight_periodic line 465
  46. lemma OAI.StrictHotSpots.Helmholtz.integral_weight_deriv line 469
  47. lemma OAI.StrictHotSpots.Helmholtz.circleMap_mem_ball line 484
  48. lemma OAI.StrictHotSpots.Helmholtz.continuous_jointCircleMap line 491
  49. lemma OAI.StrictHotSpots.Helmholtz.continuous_direction line 496
  50. lemma OAI.StrictHotSpots.Helmholtz.radial_regular line 499
  51. lemma OAI.StrictHotSpots.Helmholtz.angular_regular line 521
  52. def OAI.StrictHotSpots.Helmholtz.coeff line 545
  53. def OAI.StrictHotSpots.Helmholtz.coeffDeriv line 548
  54. def OAI.StrictHotSpots.Helmholtz.coeffSecond line 551
  55. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_coeff line 554
  56. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_coeffDeriv line 566
  57. lemma OAI.StrictHotSpots.Helmholtz.radial_periodic line 579
  58. lemma OAI.StrictHotSpots.Helmholtz.angularDeriv_periodic line 583
  59. lemma OAI.StrictHotSpots.Helmholtz.integral_weight_angularSecond line 588
  60. lemma OAI.StrictHotSpots.Helmholtz.coeff_ode line 605
  61. def OAI.StrictHotSpots.Helmholtz.circleFunction line 657
  62. lemma OAI.StrictHotSpots.Helmholtz.circleFunction_coe line 660
  63. lemma OAI.StrictHotSpots.Helmholtz.continuous_circleFunction line 664
  64. lemma OAI.StrictHotSpots.Helmholtz.coeff_zero_implies_radial_zero line 676
  65. lemma OAI.StrictHotSpots.Helmholtz.coeff_zero_of_ball_zero line 689
  66. lemma OAI.StrictHotSpots.Helmholtz.coeffDeriv_zero_of_ball_zero line 695
  67. lemma OAI.StrictHotSpots.Helmholtz.coeff_zero_on_ball line 707
  68. lemma OAI.StrictHotSpots.Helmholtz.zero_on_ball_of_zero_on_small_ball line 749
  69. theorem OAI.StrictHotSpots.Helmholtz.uniqueContinuation line 769
  70. abbrev OAI.StrictHotSpots.Helmholtz.smulFlip line 811
  71. lemma OAI.StrictHotSpots.Helmholtz.directional_convolution line 814
  72. lemma OAI.StrictHotSpots.Helmholtz.laplacian_convolution line 822
  73. lemma OAI.StrictHotSpots.Helmholtz.laplacian_reflect_translate line 852
  74. def OAI.StrictHotSpots.Helmholtz.WeakEquation line 870
  75. lemma OAI.StrictHotSpots.Helmholtz.convolution_solves line 874
  76. def OAI.StrictHotSpots.Helmholtz.mollifier line 895
  77. lemma OAI.StrictHotSpots.Helmholtz.mollifier_radius_tendsto line 901
  78. def OAI.StrictHotSpots.Helmholtz.smoothen line 905
  79. lemma OAI.StrictHotSpots.Helmholtz.smoothen_contDiff line 907
  80. lemma OAI.StrictHotSpots.Helmholtz.smoothen_tendsto line 912
  81. lemma OAI.StrictHotSpots.Helmholtz.reflected_mollifier_support line 920
  82. lemma OAI.StrictHotSpots.Helmholtz.smoothen_PDE line 931
  83. lemma OAI.StrictHotSpots.Helmholtz.smoothen_zero line 944
  84. lemma OAI.StrictHotSpots.Helmholtz.weak_zero_on_ball line 963
  85. lemma OAI.StrictHotSpots.Helmholtz.WeakEquation.mono line 985
  86. theorem OAI.StrictHotSpots.Helmholtz.weak_uniqueContinuation line 992
  87. abbrev OAI.StrictHotSpots.planeBasis line 1052
  88. def OAI.StrictHotSpots.directionalDerivative line 1054
  89. lemma OAI.StrictHotSpots.directionalDerivative_contDiffOn line 1057
  90. lemma OAI.StrictHotSpots.laplacian_eq_sum_directional line 1062
  91. def OAI.StrictHotSpots.PlaneWeakEquation line 1089
  92. lemma OAI.StrictHotSpots.weak_laplacian_test line 1093
  93. lemma OAI.StrictHotSpots.planeWeakEquation_of_euler line 1123
  94. lemma OAI.StrictHotSpots.InFirstNeumannEigenspace.planeWeakEquation line 1131
  95. def OAI.StrictHotSpots.coord line 1146
  96. def OAI.StrictHotSpots.complexExtension line 1148
  97. lemma OAI.StrictHotSpots.complexExtension_integral line 1151
  98. lemma OAI.StrictHotSpots.complexExtension_integrable line 1165
  99. lemma OAI.StrictHotSpots.complexExtension_weak line 1172
  100. theorem OAI.StrictHotSpots.planeWeak_uniqueContinuation line 1192