OAI/Probability/GaussianInformation/Kernel/JointRules.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.DriftTools.FiniteReference.kernel_average_measurable line 17
2. lemma OAI.KernelPotential.DriftTools.FiniteReference.kernel_average_integrable line 30
3. def OAI.KernelPotential.NoisyDrift.postCharge line 48
4. lemma OAI.KernelPotential.NoisyDrift.measurable_postCharge line 52
5. lemma OAI.KernelPotential.NoisyDrift.postCharge_uniform_bound line 63
6. lemma OAI.KernelPotential.NoisyDrift.postCharge_pointwise line 78
7. lemma OAI.KernelPotential.NoisyDrift.integrable_postCharge_average line 97
8. lemma OAI.KernelPotential.NoisyDrift.integrated_postCharge line 114