OAI/Probability/GaussianInformation/Kernel/Coercivity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Coercivity.inverse_kernel_bound line 13
2. lemma OAI.KernelPotential.Coercivity.integral_square_le line 45
3. lemma OAI.KernelPotential.Coercivity.measurable_kernel line 56
4. lemma OAI.KernelPotential.Coercivity.measurable_J line 60
5. lemma OAI.KernelPotential.Coercivity.J_square_integral line 65
6. lemma OAI.KernelPotential.Coercivity.bounded_density_representation line 86
7. lemma OAI.KernelPotential.Coercivity.bounded_J line 111
8. lemma OAI.KernelPotential.Coercivity.lower_J_on_sphere line 126
9. lemma OAI.KernelPotential.Coercivity.integrable_log_of_bounds line 140
10. lemma OAI.KernelPotential.Coercivity.J_real_bounds line 158
11. lemma OAI.KernelPotential.Coercivity.integrable_log_J line 173
12. lemma OAI.KernelPotential.Coercivity.density_integral_one line 184
13. lemma OAI.KernelPotential.Coercivity.density_entropy_nonneg line 195
14. lemma OAI.KernelPotential.Coercivity.entropy_young line 208
15. def OAI.KernelPotential.Coercivity.sphereMoment line 217
16. lemma OAI.KernelPotential.Coercivity.sphereMoment_pos line 218
17. lemma OAI.KernelPotential.Coercivity.square_integrable_bound line 220
18. lemma OAI.KernelPotential.Coercivity.Phi_density_formula line 237
19. lemma OAI.KernelPotential.Coercivity.B_entropy_bound line 257
20. lemma OAI.KernelPotential.Coercivity.log_sphereMoment_le line 298
21. lemma OAI.KernelPotential.Coercivity.coercivity line 317
22. lemma OAI.KernelPotential.Coercivity.Phi_uniform_le line 325