OAI/Analysis/CoulombIonization/ThomasFermi/PatchCoulombControl.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAnalysis.tfCoulombL_pair_sq_le line 16
  2. lemma OAI.CoulombAnalysis.tfPatchGap_coulomb_le line 27
  3. theorem OAI.CoulombAnalysis.tfPatchGap_pair_control line 36
  4. lemma OAI.CoulombAnalysis.compact_partial_integration_by_parts line 47
  5. def OAI.CoulombAnalysis.tfPartial line 62
  6. lemma OAI.CoulombAnalysis.tfPartial_contDiff line 65
  7. lemma OAI.CoulombAnalysis.tfPartial_continuous line 69
  8. lemma OAI.CoulombAnalysis.tfPartial_compact line 73
  9. lemma OAI.CoulombAnalysis.tfLaplacian_eq line 76
  10. lemma OAI.CoulombAnalysis.tfLaplacian_continuous line 88
  11. lemma OAI.CoulombAnalysis.tfLaplacian_compact line 93
  12. lemma OAI.CoulombAnalysis.compact_second_partial_green line 105
  13. theorem OAI.CoulombAnalysis.compact_laplacian_green line 120
  14. theorem OAI.CoulombAnalysis.compact_laplacian_energy line 136