OAI/Analysis/CoulombIonization/FieldAnalysis/RotationTrace.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.sum_norm_sq_basis_eq line 17
  2. lemma OAI.CoulombNeumann.sum_norm_sq_basis_isometry line 40
  3. def OAI.CoulombNeumann.particleRotation line 57
  4. def OAI.CoulombNeumann.flatRotation line 60
  5. lemma OAI.CoulombNeumann.flatRotation_apply line 64
  6. lemma OAI.CoulombNeumann.particleRotation_preserving line 68
  7. lemma OAI.CoulombNeumann.flatRotation_preserving line 73
  8. lemma OAI.CoulombNeumann.flatRotation_anti line 78
  9. def OAI.CoulombNeumann.flatInsertion line 85
  10. lemma OAI.CoulombNeumann.flatInsertion_apply line 88
  11. lemma OAI.CoulombNeumann.flatInsertion_basis line 93
  12. lemma OAI.CoulombNeumann.flatRotation_insertion line 103
  13. lemma OAI.CoulombNeumann.flatRotation_trace line 113
  14. lemma OAI.CoulombNeumann.memLp_fderiv_apply line 123
  15. lemma OAI.CoulombNeumann.flatRotation_fderiv line 137
  16. lemma OAI.CoulombNeumann.flatRotation_gradient_memLp line 146
  17. lemma OAI.CoulombNeumann.flatRotation_kinetic line 153