OAI/Analysis/HotSpots/Dirichlet.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.LpZeroExtension.integral_inner line 14
  2. lemma OAI.StrictHotSpots.LpZeroExtension.integral_mul line 23
  3. lemma OAI.StrictHotSpots.LpZeroExtension.integrable line 27
  4. lemma OAI.StrictHotSpots.LpZeroExtension.weak_of_neumann line 40
  5. lemma OAI.StrictHotSpots.LpZeroExtension.zero_of_weak line 52
  6. lemma OAI.StrictHotSpots.H10.zero_of_neumann line 90
  7. lemma OAI.StrictHotSpots.smoothTest_value_sq_global line 107
  8. lemma OAI.StrictHotSpots.smoothTest_grad_sq_global line 120
  9. lemma OAI.StrictHotSpots.gradient_comp_smul line 133
  10. lemma OAI.StrictHotSpots.H10.radius_pos line 149
  11. def OAI.StrictHotSpots.H10.dilateTest line 151
  12. lemma OAI.StrictHotSpots.H10.dilateTest_value_sq line 166
  13. lemma OAI.StrictHotSpots.H10.dilateTest_grad_sq line 175
  14. lemma OAI.StrictHotSpots.H10.dilateTest_norm line 189
  15. lemma OAI.StrictHotSpots.compact_of_norm_dominated line 206
  16. def OAI.StrictHotSpots.H10.dilation line 246
  17. lemma OAI.StrictHotSpots.H10.dilation_test line 249
  18. lemma OAI.StrictHotSpots.H10.dilation_value_sq line 257
  19. lemma OAI.StrictHotSpots.H10.le_mul_of_inv_sq line 268
  20. lemma OAI.StrictHotSpots.H10.value_dilation_bound line 273
  21. lemma OAI.StrictHotSpots.H10.value_compact_of_ball line 279
  22. lemma OAI.StrictHotSpots.H10.value_compact line 287
  23. lemma OAI.StrictHotSpots.positive_norm_mem_spectrum line 300
  24. lemma OAI.StrictHotSpots.positive_compact_top_eigenvector line 321
  25. lemma OAI.StrictHotSpots.DirichletOperator.energy_nonneg line 348
  26. lemma OAI.StrictHotSpots.DirichletOperator.energy_eq_zero line 354
  27. lemma OAI.StrictHotSpots.DirichletOperator.green_ne_zero line 363
  28. lemma OAI.StrictHotSpots.DirichletOperator.minimum_attained line 377
  29. lemma OAI.StrictHotSpots.H10.value_ne_zero line 428
  30. lemma OAI.StrictHotSpots.H10.minimum line 443
  31. def OAI.StrictHotSpots.H1.corrected line 471
  32. lemma OAI.StrictHotSpots.H1.mean_corrected line 472
  33. lemma OAI.StrictHotSpots.H1.corrected_form line 477
  34. lemma OAI.StrictHotSpots.PlaneWaves.all_pair_zero line 485
  35. def OAI.StrictHotSpots.PlaneWaves.frequency line 522
  36. lemma OAI.StrictHotSpots.PlaneWaves.frequency_norm_sq line 523
  37. lemma OAI.StrictHotSpots.PlaneWaves.frequency_inner line 527
  38. lemma OAI.StrictHotSpots.PlaneWaves.frequency_continuous line 530
  39. lemma OAI.StrictHotSpots.PlaneWaves.cosine_integral_continuous line 536
  40. lemma OAI.StrictHotSpots.PlaneWaves.exists_nearby line 549
  41. lemma OAI.StrictHotSpots.H10.zero_of_form_neumann line 583
  42. lemma OAI.StrictHotSpots.H10.strict_gap line 602
  43. lemma OAI.StrictHotSpots.H10.subcritical line 624