OAI/Probability/GaussianInformation/Kernel/NoiseLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.Noise.noiseLaw line 12
2. lemma OAI.KernelPotential.Noise.measurable_noise_density line 15
3. lemma OAI.KernelPotential.Noise.noise_probability line 18
4. lemma OAI.KernelPotential.Noise.noise_support line 23
5. lemma OAI.KernelPotential.Noise.boxScale_pos line 29
6. lemma OAI.KernelPotential.Noise.boxScale_ne_top line 33
7. lemma OAI.KernelPotential.Noise.boxScale_dilate line 37
8. lemma OAI.KernelPotential.Noise.shifted_box_le line 50
9. def OAI.KernelPotential.Noise.projectedReference line 69
10. lemma OAI.KernelPotential.Noise.projectedReference_measurable line 73
11. lemma OAI.KernelPotential.Noise.projectedReference_le line 82
12. lemma OAI.KernelPotential.Noise.projectedReference_shift_le line 90