OAI/Probability/GaussianInformation/Kernel/JointCompensation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.DriftTools.FiniteReference.joint line 16
2. lemma OAI.KernelPotential.DriftTools.FiniteReference.joint_integral_nonneg line 20
3. lemma OAI.KernelPotential.DriftTools.FiniteReference.joint_probability line 38
4. def OAI.KernelPotential.DriftTools.FiniteReference.C line 47
5. lemma OAI.KernelPotential.DriftTools.FiniteReference.measurable_C line 50
6. lemma OAI.KernelPotential.DriftTools.FiniteReference.joint_compensation line 60
7. lemma OAI.KernelPotential.DriftTools.FiniteReference.log_comparison line 87