OAI/Analysis/CoulombIonization/FieldAnalysis/NeumannReindex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.integral_cube_reindex line 19
  2. lemma OAI.CoulombNeumann.cubeNeumannMode_reindex line 32
  3. def OAI.CoulombNeumann.realReindex line 38
  4. lemma OAI.CoulombNeumann.realReindex_apply line 42
  5. lemma OAI.CoulombNeumann.realReindex_single line 49
  6. def OAI.CoulombNeumann.finiteCubeFunction line 56
  7. def OAI.CoulombNeumann.finiteCubeGradient line 60
  8. lemma OAI.CoulombNeumann.finiteCubeFunction_reindex line 65
  9. lemma OAI.CoulombNeumann.finiteCubeGradient_reindex line 70
  10. lemma OAI.CoulombNeumann.neumannCoeff_reindex line 81
  11. lemma OAI.CoulombNeumann.cubeGradient_eq_finite line 93
  12. theorem OAI.CoulombNeumann.finite_neumann_spectral_lower line 101
  13. lemma OAI.CoulombNeumann.integral_cube_permute line 146
  14. lemma OAI.CoulombNeumann.cubeNeumannMode_permute line 159
  15. abbrev OAI.CoulombNeumann.particlePermute line 167
  16. def OAI.CoulombNeumann.CubeAntisymmetric line 170
  17. lemma OAI.CoulombNeumann.coeff_zero_of_repeated_mode line 174
  18. theorem OAI.CoulombNeumann.coeff_nonzero_injective line 206