OAI/Probability/GaussianInformation/Kernel/Entropy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.EntropySupport.xlog line 11
2. lemma OAI.KernelPotential.EntropySupport.continuous_xlog line 13
3. lemma OAI.KernelPotential.EntropySupport.xlog_zero line 14
4. lemma OAI.KernelPotential.EntropySupport.xlog_one line 15
5. lemma OAI.KernelPotential.EntropySupport.xlog_mul line 16
6. lemma OAI.KernelPotential.EntropySupport.mul_log_div_le line 22
7. lemma OAI.KernelPotential.EntropySupport.xlog_lower_tangent line 30
8. lemma OAI.KernelPotential.EntropySupport.integrable_bounded_measurable line 42
9. lemma OAI.KernelPotential.EntropySupport.integrable_xlog_bounded line 48
10. lemma OAI.KernelPotential.EntropySupport.klDiv_withDensity_bounded line 56