OAI/Probability/GaussianInformation/Kernel/MassPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.MassPotential.normalized line 17
2. def OAI.KernelPotential.MassPotential.energy line 18
3. def OAI.KernelPotential.MassPotential.proper line 19
4. lemma OAI.KernelPotential.MassPotential.normalized_probability line 21
5. lemma OAI.KernelPotential.MassPotential.proper_probability line 26
6. lemma OAI.KernelPotential.MassPotential.proper_bounded line 31
7. lemma OAI.KernelPotential.MassPotential.mass_smul_proper line 43
8. lemma OAI.KernelPotential.MassPotential.energy_proper line 50
9. lemma OAI.KernelPotential.MassPotential.energy_smul_probability line 55
10. lemma OAI.KernelPotential.MassPotential.energy_mixture line 64