OAI/Probability/GaussianInformation/Kernel/DriftCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.DriftCutoff.level line 14
2. lemma OAI.KernelPotential.DriftCutoff.level_pos line 16
3. lemma OAI.KernelPotential.DriftCutoff.level_lower line 18
4. lemma OAI.KernelPotential.DriftCutoff.level_upper line 24
5. lemma OAI.KernelPotential.DriftCutoff.log_constant_bound line 32
6. lemma OAI.KernelPotential.DriftCutoff.reference_cut line 56
7. lemma OAI.KernelPotential.DriftCutoff.moment_cut line 66
8. lemma OAI.KernelPotential.DriftCutoff.log_level_bound line 79