OAI/Probability/GaussianInformation/Kernel/SampleLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Noise.boxKernel_translate line 15
2. lemma OAI.KernelPotential.Noise.lintegral_noisy_translate line 24
3. abbrev OAI.KernelPotential.Noise.Observation line 33
4. def OAI.KernelPotential.Noise.observationBase line 35
5. def OAI.KernelPotential.Noise.observationKernel line 38
6. instance OAI.KernelPotential.Noise.observationBase_sigmaFinite line 41
7. lemma OAI.KernelPotential.Noise.observationKernel_measurable line 45
8. lemma OAI.KernelPotential.Noise.observationKernel_probability line 52
9. lemma OAI.KernelPotential.Noise.observation_lintegral line 67