OAI/Analysis/CoulombRadii/Propagation/NearActiveMaximum.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NeutralAtom.WeakLaplacianGE.congr_on line 15
  2. lemma OAI.NeutralAtom.WeakLaplacianGE.mono_domain line 32
  3. theorem OAI.NeutralAtom.WeakNuclearSubsolution.near_active_cutoffTF line 36
  4. def OAI.NeutralAtom.propagationBarrier line 75
  5. lemma OAI.NeutralAtom.radialPower_half_nat line 78
  6. lemma OAI.NeutralAtom.propagationBarrier_eq line 86
  7. lemma OAI.NeutralAtom.contDiffOn_propagationBarrier line 96
  8. lemma OAI.NeutralAtom.laplacian_propagationBarrier line 101
  9. lemma OAI.NeutralAtom.tfScalarDensity_eq_kTF line 129
  10. lemma OAI.NeutralAtom.tfReaction_eq_scalar line 142
  11. lemma OAI.NeutralAtom.tfReaction_normalized line 147
  12. lemma OAI.NeutralAtom.normalized_density_le_reaction_iff line 155
  13. lemma OAI.NeutralAtom.normalized_reaction_le_density_iff line 169
  14. lemma OAI.NeutralAtom.propagation_gain_density line 183
  15. lemma OAI.NeutralAtom.propagation_outer_reaction line 211