OAI/Geometry/EinsteinFour/SineModeLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The first scalar Dirichlet eigenvalue and its radial comparison limit.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.two_sub_two_cos line 15
  2. def OAI.PositiveEinsteinFour.Jacobi.firstEigenvalue line 21
  3. def OAI.PositiveEinsteinFour.Jacobi.scaledFirstEigenvalue line 24
  4. theorem OAI.PositiveEinsteinFour.Jacobi.scaledFirstEigenvalue_eq_sinc line 27
  5. theorem OAI.PositiveEinsteinFour.Jacobi.scaledFirstEigenvalue_tendsto line 43
  6. theorem OAI.PositiveEinsteinFour.Jacobi.firstEigenvalue_eventually_pos line 61
  7. theorem OAI.PositiveEinsteinFour.Jacobi.first_mode_coefficient_tendsto line 68