OAI/Analysis/CoulombIonization/FieldAnalysis/NeumannPhysical.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.cartesianValue line 19
  2. def OAI.CoulombAtom.cartesianGradient line 22
  3. lemma OAI.CoulombAtom.SobolevFermion.cartesian_anti line 25
  4. lemma OAI.CoulombAtom.SobolevFermion.cartesian_weak line 32
  5. theorem OAI.CoulombAtom.SobolevFermion.neumann_unit_grid line 55
  6. theorem OAI.CoulombAtom.FormAdmissible.neumann_unit_grid line 81
  7. lemma OAI.CoulombNeumann.memLp_comp_real_smul line 102
  8. lemma OAI.CoulombNeumann.memLp_comp_affine line 108
  9. lemma OAI.CoulombNeumann.integral_comp_affine line 112
  10. def OAI.CoulombNeumann.gridTranslation line 121
  11. def OAI.CoulombNeumann.affineGrid line 123
  12. def OAI.CoulombNeumann.affineGridInv line 126
  13. lemma OAI.CoulombNeumann.affineGridInv_affineGrid line 129
  14. lemma OAI.CoulombNeumann.affineGrid_affineGridInv line 133
  15. lemma OAI.CoulombNeumann.affineGrid_anti line 137
  16. lemma OAI.CoulombNeumann.affineGrid_contDiff line 144
  17. lemma OAI.CoulombNeumann.affineGrid_fderiv line 149
  18. def OAI.CoulombNeumann.gridPressure line 159
  19. lemma OAI.CoulombNeumann.gridPressure_nonneg line 162
  20. lemma OAI.CoulombNeumann.gridPressure_bound line 165
  21. lemma OAI.CoulombNeumann.gridPressure_measurable line 169
  22. lemma OAI.CoulombNeumann.gridPressure_integrable line 176
  23. theorem OAI.CoulombNeumann.neumann_affine_smooth_component line 183