OAI/Analysis/CoulombIonization/FieldAnalysis/NeumannGradient.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombNeumann.cubeNeumannMode_split line 20
  2. lemma OAI.CoulombNeumann.cubeSineMode_split line 27
  3. lemma OAI.CoulombNeumann.coe_insertNth line 33
  4. lemma OAI.CoulombNeumann.contDiff_insertNth line 38
  5. lemma OAI.CoulombNeumann.hasDerivAt_insertNth line 44
  6. def OAI.CoulombNeumann.cubeFunction line 52
  7. def OAI.CoulombNeumann.cubeGradient line 56
  8. lemma OAI.CoulombNeumann.deriv_slice line 61
  9. lemma OAI.CoulombNeumann.cube_derivative_pairing line 68
  10. lemma OAI.CoulombNeumann.continuous_toLp_norm_sq line 95
  11. def OAI.CoulombNeumann.neumannCoeff line 105
  12. lemma OAI.CoulombNeumann.neumannCoeff_eq_inner line 108
  13. lemma OAI.CoulombNeumann.neumann_parseval line 113
  14. lemma OAI.CoulombNeumann.neumannCoeff_summable line 122
  15. lemma OAI.CoulombNeumann.neumann_derivative_bessel line 129
  16. theorem OAI.CoulombNeumann.neumann_spectral_lower line 145