OAI/Analysis/HotSpots/Variational.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictHotSpots.MainTheorem line 18
  2. lemma OAI.StrictHotSpots.rayleighValues_nonneg line 23
  3. lemma OAI.StrictHotSpots.firstPositiveNeumannValue_nonneg line 28
  4. lemma OAI.StrictHotSpots.rayleigh_inequality line 33
  5. lemma OAI.StrictHotSpots.eigenfunction_energy_identity line 43
  6. lemma OAI.StrictHotSpots.strict_boundary_extrema_of_noncritical line 51
  7. lemma OAI.StrictHotSpots.eigenfunction_mass_pos line 95
  8. lemma OAI.StrictHotSpots.eigenfunction_gradient_continuous line 111
  9. lemma OAI.StrictHotSpots.firstPositiveNeumannValue_pos_of_eigenfunction line 118
  10. lemma OAI.StrictHotSpots.integrable_inner_of_memLp line 152
  11. lemma OAI.StrictHotSpots.integral_norm_add_smul_sq line 158
  12. lemma OAI.StrictHotSpots.integral_sq_add_mul line 178
  13. lemma OAI.StrictHotSpots.rayleigh_inequality_all line 185
  14. lemma OAI.StrictHotSpots.minimizer_euler_mean_zero line 196
  15. lemma OAI.StrictHotSpots.minimizer_euler line 228
  16. lemma OAI.StrictHotSpots.inFirstNeumannEigenspace_of_minimizer line 258
  17. lemma OAI.StrictHotSpots.integral_mul_test_hasFDerivAt line 276
  18. lemma OAI.StrictHotSpots.HasH1Gradient.of_hasFDerivAt line 305
  19. def OAI.StrictHotSpots.Douglas.planeSeries line 322
  20. def OAI.StrictHotSpots.Douglas.planeD line 325
  21. def OAI.StrictHotSpots.Douglas.planeGrad line 329
  22. lemma OAI.StrictHotSpots.Douglas.planeSeries_continuousOn line 332
  23. lemma OAI.StrictHotSpots.Douglas.planeD_continuousOn line 339
  24. lemma OAI.StrictHotSpots.Douglas.planeGrad_continuousOn line 348
  25. lemma OAI.StrictHotSpots.Douglas.planeSeries_hasFDerivAt line 353
  26. lemma OAI.StrictHotSpots.Douglas.disk_memLp_of_continuousOn line 362
  27. theorem OAI.StrictHotSpots.Douglas.planeSeries_hasH1Gradient line 373
  28. lemma OAI.StrictHotSpots.Douglas.planeSeries_gradient line 385
  29. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_re_poisson line 410
  30. lemma OAI.StrictHotSpots.Douglas.poissonAverage_contDiffOn line 426
  31. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_re_contDiffOn line 447
  32. lemma OAI.StrictHotSpots.Douglas.planeSeries_contDiffOn line 455
  33. def OAI.StrictHotSpots.PlaneWaves.cosine line 469
  34. def OAI.StrictHotSpots.PlaneWaves.sine line 470
  35. lemma OAI.StrictHotSpots.PlaneWaves.cosine_smooth line 472
  36. lemma OAI.StrictHotSpots.PlaneWaves.sine_smooth line 474
  37. lemma OAI.StrictHotSpots.PlaneWaves.fderiv_cosine line 477
  38. lemma OAI.StrictHotSpots.PlaneWaves.fderiv_sine line 480
  39. lemma OAI.StrictHotSpots.PlaneWaves.gradient_cosine line 484
  40. lemma OAI.StrictHotSpots.PlaneWaves.gradient_sine line 489
  41. lemma OAI.StrictHotSpots.PlaneWaves.cosine_memLp line 495
  42. lemma OAI.StrictHotSpots.PlaneWaves.sine_memLp line 500
  43. lemma OAI.StrictHotSpots.PlaneWaves.cosine_h1 line 506
  44. lemma OAI.StrictHotSpots.PlaneWaves.sine_h1 line 513
  45. lemma OAI.StrictHotSpots.PlaneWaves.cosine_sine_sq line 521
  46. lemma OAI.StrictHotSpots.PlaneWaves.laplacian_cosine line 524
  47. lemma OAI.StrictHotSpots.PlaneWaves.laplacian_sine line 544
  48. lemma OAI.StrictHotSpots.lower_rayleigh line 571
  49. lemma OAI.StrictHotSpots.lower_euler_mean_zero line 579
  50. lemma OAI.StrictHotSpots.lower_euler line 612
  51. lemma OAI.StrictHotSpots.L2Inner.toLp_pair line 651
  52. lemma OAI.StrictHotSpots.L2Inner.toLp_left line 659
  53. lemma OAI.StrictHotSpots.L2Inner.toLp_right line 667
  54. lemma OAI.StrictHotSpots.two_inner_sub_left line 682
  55. lemma OAI.StrictHotSpots.two_inner_sub_right line 688
  56. def OAI.StrictHotSpots.H1.form line 698
  57. lemma OAI.StrictHotSpots.H1.form_symm line 701
  58. lemma OAI.StrictHotSpots.H1.form_sub_left line 704
  59. lemma OAI.StrictHotSpots.H1.form_sub_right line 707
  60. lemma OAI.StrictHotSpots.H1.form_smul_left line 710
  61. lemma OAI.StrictHotSpots.H1.form_smul_right line 716
  62. lemma OAI.StrictHotSpots.H1.form_diag_sub line 722
  63. def OAI.StrictHotSpots.H1.mean line 730
  64. lemma OAI.StrictHotSpots.H1.mean_eq line 734
  65. lemma OAI.StrictHotSpots.H1.form_self_integral line 740
  66. lemma OAI.StrictHotSpots.H1.form_nonneg line 744
  67. lemma OAI.StrictHotSpots.H1.form_zero_euler line 749
  68. def OAI.StrictHotSpots.CompactRows.rowOperator line 770
  69. lemma OAI.StrictHotSpots.CompactRows.rowOperator_apply_ae line 773
  70. lemma OAI.StrictHotSpots.CompactRows.rowOperator_compact_simple line 777
  71. theorem OAI.StrictHotSpots.CompactRows.rowOperator_compact line 800
  72. lemma OAI.StrictHotSpots.CompactRows.measurable_of_dist line 816
  73. lemma OAI.StrictHotSpots.CompactRows.measurable_toLp_rows line 839
  74. lemma OAI.StrictHotSpots.CompactCoercive.finite_projection_approx line 869
  75. lemma OAI.StrictHotSpots.CompactCoercive.observation_compact line 890
  76. def OAI.StrictHotSpots.PlaneGreen.boundedKernel line 974
  77. lemma OAI.StrictHotSpots.PlaneGreen.boundedKernel_measurable line 978
  78. lemma OAI.StrictHotSpots.PlaneGreen.boundedKernel_memLp line 981
  79. def OAI.StrictHotSpots.PlaneGreen.compactRow line 988
  80. lemma OAI.StrictHotSpots.PlaneGreen.compactRow_memLp line 991
  81. lemma OAI.StrictHotSpots.PlaneGreen.integralOperator_compact line 1003
  82. lemma OAI.StrictHotSpots.PlaneGreen.value_compact line 1026
  83. def OAI.StrictHotSpots.smoothTestToH10 line 1045
  84. lemma OAI.StrictHotSpots.dense_smoothTestToH10 line 1049
  85. def OAI.StrictHotSpots.H10.includeTest line 1061
  86. lemma OAI.StrictHotSpots.H10.includeTest_norm line 1066
  87. def OAI.StrictHotSpots.H10.inclusion line 1089
  88. lemma OAI.StrictHotSpots.H10.inclusion_test line 1092
  89. def OAI.StrictHotSpots.H10.restriction line 1101
  90. lemma OAI.StrictHotSpots.H10.value_inclusion line 1105
  91. lemma OAI.StrictHotSpots.H10.value_compact_of_subset line 1123
  92. lemma OAI.StrictHotSpots.H10.helmholtz_pair line 1141