OAI/Analysis/CoulombIonization/Variational/WeightedVariance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.weighted_integral_norm_sq_le line 16
2. lemma OAI.CoulombAtom.integral_le_of_nonneg_ae_limit line 48
3. lemma OAI.CoulombAtom.convolution_l2_contraction line 77
4. lemma OAI.CoulombAtom.mollified_weak_derivative line 104
5. def OAI.CoulombAtom.shrinkingBump line 132
6. lemma OAI.CoulombAtom.shrinkingBump_tendsto line 142
7. lemma OAI.CoulombAtom.weak_square_completion_bound line 147
8. lemma OAI.CoulombAtom.regularized_nuclear_bound line 207
9. lemma OAI.CoulombAtom.regularizedCoulomb_tendsto line 261
10. lemma OAI.CoulombAtom.nuclear_bound line 277
11. theorem OAI.CoulombAtom.formEnergy_lower_bound line 317
12. theorem OAI.CoulombAtom.sector_energies_bddBelow line 349