OAI/Analysis/CoulombIonization/FieldAnalysis/NeumannCube.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.cosMode_natAbs line 17
  2. lemma OAI.CoulombNeumann.cosMode_mul line 27
  3. def OAI.CoulombNeumann.cubeCosMode line 39
  4. lemma OAI.CoulombNeumann.cubeCosMode_zero line 43
  5. lemma OAI.CoulombNeumann.cubeCosMode_mul line 47
  6. def OAI.CoulombNeumann.cosineSpan line 65
  7. lemma OAI.CoulombNeumann.cubeCosMode_mem line 68
  8. lemma OAI.CoulombNeumann.cosineSpan_one line 71
  9. lemma OAI.CoulombNeumann.cosineSpan_mul line 75
  10. lemma OAI.CoulombNeumann.cubeCosMode_star line 93
  11. lemma OAI.CoulombNeumann.cosineSpan_star line 97
  12. def OAI.CoulombNeumann.cosineAlgebra line 107
  13. lemma OAI.CoulombNeumann.cubeCosMode_single line 118
  14. lemma OAI.CoulombNeumann.cosineAlgebra_separatesPoints line 127
  15. lemma OAI.CoulombNeumann.cosineSpan_dense line 140
  16. def OAI.CoulombNeumann.cubeNeumannMode line 152
  17. lemma OAI.CoulombNeumann.cosNormalization_pos line 156
  18. lemma OAI.CoulombNeumann.cubeNeumannMode_eq line 160
  19. lemma OAI.CoulombNeumann.cubeNeumannMode_span line 166
  20. lemma OAI.CoulombNeumann.cubeNeumannMode_inner line 183
  21. abbrev OAI.CoulombNeumann.neumannLp line 195
  22. lemma OAI.CoulombNeumann.orthonormal_neumann line 198
  23. lemma OAI.CoulombNeumann.neumannLp_span_dense line 205
  24. def OAI.CoulombNeumann.neumannBasis line 211
  25. lemma OAI.CoulombNeumann.neumannBasis_apply line 214