OAI/Analysis/HotSpots/Eigenfunction.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.Helmholtz.radial_ode_zero line 15
  2. lemma OAI.StrictHotSpots.Helmholtz.radial_regular_global line 79
  3. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_coeff_global line 91
  4. lemma OAI.StrictHotSpots.Helmholtz.hasDerivAt_coeffDeriv_global line 102
  5. lemma OAI.StrictHotSpots.Helmholtz.weight_zero line 114
  6. lemma OAI.StrictHotSpots.Helmholtz.coeff_center line 116
  7. lemma OAI.StrictHotSpots.Helmholtz.integral_direction line 120
  8. lemma OAI.StrictHotSpots.Helmholtz.coeffDeriv_center line 131
  9. lemma OAI.StrictHotSpots.Helmholtz.coeff_radial_ode line 137
  10. lemma OAI.StrictHotSpots.Helmholtz.circle_mean_comparison line 158
  11. def OAI.StrictHotSpots.Helmholtz.referenceReal line 194
  12. def OAI.StrictHotSpots.Helmholtz.referenceSin line 195
  13. def OAI.StrictHotSpots.Helmholtz.reference line 196
  14. lemma OAI.StrictHotSpots.Helmholtz.referenceReal_smooth line 198
  15. lemma OAI.StrictHotSpots.Helmholtz.referenceSin_smooth line 200
  16. lemma OAI.StrictHotSpots.Helmholtz.reference_smooth line 202
  17. lemma OAI.StrictHotSpots.Helmholtz.fderiv_referenceReal line 205
  18. lemma OAI.StrictHotSpots.Helmholtz.fderiv_referenceSin line 208
  19. lemma OAI.StrictHotSpots.Helmholtz.laplacian_referenceReal line 212
  20. lemma OAI.StrictHotSpots.Helmholtz.laplacian_reference line 224
  21. lemma OAI.StrictHotSpots.Helmholtz.reference_zero line 231
  22. lemma OAI.StrictHotSpots.Helmholtz.coeff_zero_eq_average line 234
  23. lemma OAI.StrictHotSpots.Helmholtz.mean_eq_reference line 239
  24. lemma OAI.StrictHotSpots.Helmholtz.radial_average_helmholtz line 266
  25. lemma OAI.StrictHotSpots.Helmholtz.regularizing_coefficient_pos line 315
  26. lemma OAI.StrictHotSpots.Helmholtz.exists_regularizing_radius line 337
  27. lemma OAI.StrictHotSpots.Helmholtz.regularizing_coefficient_eq line 359
  28. theorem OAI.StrictHotSpots.Helmholtz.local_representative line 366
  29. theorem OAI.StrictHotSpots.Helmholtz.representative line 408
  30. def OAI.StrictHotSpots.Helmholtz.coord line 456
  31. def OAI.StrictHotSpots.Helmholtz.complexExtension line 458
  32. lemma OAI.StrictHotSpots.Helmholtz.complexExtension_integral line 461
  33. lemma OAI.StrictHotSpots.Helmholtz.complexExtension_integrable line 475
  34. lemma OAI.StrictHotSpots.Helmholtz.complexExtension_weak line 482
  35. theorem OAI.StrictHotSpots.Helmholtz.plane_representative line 502
  36. lemma OAI.StrictHotSpots.HasH1Gradient.smooth_representative line 529
  37. def OAI.StrictHotSpots.InInteriorNeumannEigenspace line 572
  38. lemma OAI.StrictHotSpots.InFirstNeumannEigenspace.interior line 579
  39. theorem OAI.StrictHotSpots.weak_eigenfunction_representative line 585
  40. theorem OAI.StrictHotSpots.Hodge.vector_equality_interior line 625
  41. theorem OAI.StrictHotSpots.Hodge.vector_equality_interior_pointwise line 650
  42. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitzMultipliedGradient_closed line 687
  43. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitzMultipliedGradient_null line 739
  44. lemma OAI.StrictHotSpots.InInteriorNeumannEigenspace.congr_on line 771
  45. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.exists_lipschitz_potential line 804
  46. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.null_eigenfunction_lipschitz line 835
  47. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.coordinate_null_trace line 864
  48. lemma OAI.StrictHotSpots.InInteriorNeumannEigenspace.differentiableAt line 918
  49. lemma OAI.StrictHotSpots.gradient_add_at line 923
  50. lemma OAI.StrictHotSpots.gradient_smul_at line 928
  51. lemma OAI.StrictHotSpots.InInteriorNeumannEigenspace.add line 932
  52. lemma OAI.StrictHotSpots.InInteriorNeumannEigenspace.smul line 967
  53. lemma OAI.StrictHotSpots.InInteriorNeumannEigenspace.zero line 990
  54. abbrev OAI.StrictHotSpots.ClosedEigenJet line 1005
  55. def OAI.StrictHotSpots.closedEigenJet line 1007
  56. def OAI.StrictHotSpots.closedEigenSpace line 1013
  57. lemma OAI.StrictHotSpots.closedEigenJet_eq_zero_of_eqOn line 1034
  58. lemma OAI.StrictHotSpots.closedEigenJet_nonzero_interior line 1049