OAI/Analysis/CoulombIonization/Fermionic/FreqCut.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombLT.l2_norm_sq_eq_integral line 25
  2. lemma OAI.CoulombLT.l2_ball_integrable line 34
  3. def OAI.CoulombLT.freqCut line 41
  4. lemma OAI.CoulombLT.freqCut_ae line 44
  5. def OAI.CoulombLT.lowPart line 48
  6. lemma OAI.CoulombLT.lowPart_continuous line 51
  7. lemma OAI.CoulombLT.lowPart_ae line 60
  8. lemma OAI.CoulombLT.freqCut_norm_sq line 65
  9. lemma OAI.CoulombLT.highPart_norm_sq line 74
  10. def OAI.CoulombLT.kernelFunction line 106
  11. lemma OAI.CoulombLT.kernelFunction_memLp line 109
  12. def OAI.CoulombLT.lowKernel line 118
  13. lemma OAI.CoulombLT.lowKernel_norm_sq line 121
  14. lemma OAI.CoulombLT.lowPart_eq_inner line 133
  15. def OAI.CoulombLT.BesselFamily line 145
  16. lemma OAI.CoulombLT.BesselFamily.fourier line 148
  17. lemma OAI.CoulombLT.BesselFamily.low_bound line 158
  18. lemma OAI.CoulombLT.family_density_split line 163