OAI/Probability/GaussianInformation/Kernel/EntropyDrift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.DriftTools.compensated_log_bound line 11
2. lemma OAI.KernelPotential.DriftTools.compensation_lintegral line 50
3. lemma OAI.KernelPotential.DriftTools.log_young line 81
4. lemma OAI.KernelPotential.DriftTools.weighted_log_moment line 94
5. lemma OAI.KernelPotential.DriftTools.integral_log_le_log_of_integral_le line 120
6. lemma OAI.KernelPotential.DriftTools.pow_one_add_le line 143
7. lemma OAI.KernelPotential.DriftTools.integrable_of_bounded line 155
8. lemma OAI.KernelPotential.DriftTools.integral_weighted_log_moment line 160