OAI/Analysis/HotSpots/Sobolev.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.existsUnique_of_coercive line 17
  2. lemma OAI.StrictHotSpots.test_memLp line 42
  3. lemma OAI.StrictHotSpots.test_derivative_memLp line 48
  4. lemma OAI.StrictHotSpots.HasH1Gradient.add line 54
  5. lemma OAI.StrictHotSpots.HasH1Gradient.smul line 72
  6. lemma OAI.StrictHotSpots.HasH1Gradient.sub line 82
  7. lemma OAI.StrictHotSpots.integral_test_derivative_zero line 87
  8. lemma OAI.StrictHotSpots.HasH1Gradient.const line 100
  9. lemma OAI.StrictHotSpots.integrable_mul_test line 115
  10. lemma OAI.StrictHotSpots.setIntegral_mul_test line 124
  11. lemma OAI.StrictHotSpots.integral_mul_test_fderiv line 131
  12. lemma OAI.StrictHotSpots.HasH1Gradient.of_contDiffOn line 151
  13. lemma OAI.StrictHotSpots.test_gradient_memLp line 160
  14. lemma OAI.StrictHotSpots.HasH1Gradient.test line 170
  15. lemma OAI.StrictHotSpots.test_vector_memLp line 176
  16. structure OAI.StrictHotSpots.H1Test line 183
  17. def OAI.StrictHotSpots.H1Test.scalar line 191
  18. def OAI.StrictHotSpots.H1Test.derivative line 194
  19. def OAI.StrictHotSpots.H1Test.vector line 197
  20. abbrev OAI.StrictHotSpots.H1Ambient line 201
  21. def OAI.StrictHotSpots.h1Graph line 205
  22. lemma OAI.StrictHotSpots.h1Graph_closed line 218
  23. abbrev OAI.StrictHotSpots.H1 line 230
  24. instance OAI.StrictHotSpots.H1.completeSpace line 232
  25. lemma OAI.StrictHotSpots.h1Graph_mem_iff line 235
  26. lemma OAI.StrictHotSpots.HasH1Gradient.congr line 263
  27. def OAI.StrictHotSpots.HasH1Gradient.toH1 line 280
  28. def OAI.StrictHotSpots.H1.value line 287
  29. def OAI.StrictHotSpots.H1.grad line 290
  30. lemma OAI.StrictHotSpots.H1.hasH1Gradient line 293
  31. lemma OAI.StrictHotSpots.H1.norm_sq line 296
  32. lemma OAI.StrictHotSpots.H1.value_toH1 line 299
  33. lemma OAI.StrictHotSpots.H1.grad_toH1 line 302
  34. lemma OAI.StrictHotSpots.H1.grad_unique line 305
  35. lemma OAI.StrictHotSpots.H1.value_injective line 334
  36. def OAI.StrictHotSpots.smoothTestSpace line 345
  37. def OAI.StrictHotSpots.smoothTestToH1 line 359
  38. lemma OAI.StrictHotSpots.smoothTestToH1_value_norm line 369
  39. lemma OAI.StrictHotSpots.smoothTestToH1_grad_norm line 378
  40. def OAI.StrictHotSpots.h10Submodule line 388
  41. abbrev OAI.StrictHotSpots.H10 line 391
  42. instance OAI.StrictHotSpots.H10.normedAddCommGroup line 393
  43. instance OAI.StrictHotSpots.H10.innerProductSpace line 396
  44. instance OAI.StrictHotSpots.H10.completeSpace line 399
  45. lemma OAI.StrictHotSpots.test_sobolev_ennreal line 404
  46. lemma OAI.StrictHotSpots.eLpNorm_fderiv_le_L2_gradient line 422
  47. lemma OAI.StrictHotSpots.test_poincare_ennreal line 443
  48. lemma OAI.StrictHotSpots.test_poincare_real line 456
  49. lemma OAI.StrictHotSpots.smoothTest_poincare line 475
  50. lemma OAI.StrictHotSpots.norm_bound_on_closure line 489
  51. def OAI.StrictHotSpots.H10.value line 503
  52. def OAI.StrictHotSpots.H10.grad line 506
  53. lemma OAI.StrictHotSpots.H10.norm_sq line 509
  54. lemma OAI.StrictHotSpots.H10.poincare line 512
  55. def OAI.StrictHotSpots.H10.energy line 524
  56. lemma OAI.StrictHotSpots.H10.energy_apply line 534
  57. lemma OAI.StrictHotSpots.H10.energy_coercive line 537
  58. lemma OAI.StrictHotSpots.H10.existsUnique_energy_solution line 555
  59. lemma OAI.StrictHotSpots.H10.existsUnique_dirichlet_solution line 563
  60. lemma OAI.StrictHotSpots.DiskCutoff.transition_deriv_zero line 579
  61. lemma OAI.StrictHotSpots.DiskCutoff.transition_deriv_bound line 591
  62. def OAI.StrictHotSpots.DiskCutoff.cutoff line 605
  63. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_nonneg line 608
  64. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_le_one line 611
  65. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_zero line 614
  66. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_one line 620
  67. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_tsupport line 623
  68. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_tsupport_disk line 631
  69. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_hasCompactSupport line 641
  70. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_contDiff line 648
  71. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_fderiv line 652
  72. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_fderiv_zero line 665
  73. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_eventually_one line 670
  74. lemma OAI.StrictHotSpots.DiskCutoff.boundary_vanishing_estimate line 679
  75. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_mul_contDiff line 703
  76. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_mul_hasCompactSupport line 719
  77. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_mul_norm_le line 724
  78. lemma OAI.StrictHotSpots.DiskCutoff.cutoff_mul_fderiv_bound line 729
  79. lemma OAI.StrictHotSpots.L2VectorLimits.norm_sq_eq_integral_norm_sq line 765
  80. lemma OAI.StrictHotSpots.L2VectorLimits.norm_toLp_sub_sq line 770
  81. lemma OAI.StrictHotSpots.L2VectorLimits.tendsto_toLp_of_dominated line 778
  82. lemma OAI.StrictHotSpots.H1.tendsto_of_value_grad line 809
  83. def OAI.StrictHotSpots.DiskH10.disk line 826
  84. lemma OAI.StrictHotSpots.DiskH10.norm_gradient_eq line 828
  85. lemma OAI.StrictHotSpots.DiskH10.smooth_zero_boundary_bounds line 832
  86. lemma OAI.StrictHotSpots.DiskH10.smooth_memH1 line 857
  87. lemma OAI.StrictHotSpots.DiskH10.smooth_zero_boundary_memH10 line 881
  88. lemma OAI.StrictHotSpots.integral_inner_gradient_test line 942
  89. lemma OAI.StrictHotSpots.inner_toLp_toLp line 989
  90. lemma OAI.StrictHotSpots.smoothTest_value line 998
  91. lemma OAI.StrictHotSpots.smoothTest_grad line 1004
  92. lemma OAI.StrictHotSpots.smooth_weak_poisson line 1010