OAI/Analysis/CoulombRadii/FieldAnalysis/CosineWeight.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.evenOnSegment_intervalIntegrable line 14
  2. lemma OAI.Coulomb.integral_evenOnSegment line 23
  3. lemma OAI.Coulomb.complex_exp_pair line 47
  4. lemma OAI.Coulomb.cosine_natAbs line 54
  5. lemma OAI.Coulomb.fourier_pair_cosine line 61
  6. lemma OAI.Coulomb.fourierOn_evenOnSegment line 80
  7. theorem OAI.Coulomb.cosineModes_complete line 95
  8. lemma OAI.Coulomb.cosineMode_continuous line 114
  9. lemma OAI.Coulomb.cosineMode_memLp line 118
  10. lemma OAI.Coulomb.integral_cosine_product_pi line 125
  11. lemma OAI.Coulomb.integral_cosine_product line 145
  12. def OAI.Coulomb.cosineWeight line 163
  13. lemma OAI.Coulomb.cosineWeight_pos line 165
  14. lemma OAI.Coulomb.cosineMode_inner line 169
  15. def OAI.Coulomb.neumannMode line 185
  16. lemma OAI.Coulomb.neumannMode_memLp line 188
  17. lemma OAI.Coulomb.neumannMode_star line 192
  18. lemma OAI.Coulomb.neumannMode_orthonormal line 197
  19. lemma OAI.Coulomb.neumannModes_complete line 227
  20. def OAI.Coulomb.sineMode line 238
  21. lemma OAI.Coulomb.sineMode_memLp line 241
  22. lemma OAI.Coulomb.integral_cosine_nonzero line 248
  23. lemma OAI.Coulomb.integral_sine_product line 253
  24. lemma OAI.Coulomb.sineMode_inner line 283
  25. def OAI.Coulomb.dirichletMode line 300
  26. lemma OAI.Coulomb.dirichletMode_memLp line 303
  27. lemma OAI.Coulomb.dirichletMode_star line 307
  28. lemma OAI.Coulomb.dirichletMode_orthonormal line 312
  29. lemma OAI.Coulomb.dirichletMode_hasDerivAt line 337
  30. lemma OAI.Coulomb.dirichletMode_endpoints line 356
  31. lemma OAI.Coulomb.dirichletMode_continuous line 366
  32. lemma OAI.Coulomb.neumannMode_continuous line 371
  33. lemma OAI.Coulomb.neumannMode_star_self line 375
  34. lemma OAI.Coulomb.neumann_coefficient_derivative line 380
  35. theorem OAI.Coulomb.neumann_smooth_spectral_lower line 408