OAI/Probability/GaussianInformation/Kernel/PositiveRules.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KernelPotential.NoisyDrift.PositiveRule line 18
2. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.nonneg line 28
3. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.le_one line 29
4. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.measurable line 32
5. def OAI.KernelPotential.NoisyDrift.PositiveRule.kernel line 34
6. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.measurable_kernel line 36
7. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.sum_kernel line 39
8. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.kernel_le_one line 42
9. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.lower_kernel line 44
10. def OAI.KernelPotential.NoisyDrift.PositiveRule.response line 46
11. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.measurable_response line 48
12. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.response_bounds line 56
13. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.response_sum line 61
14. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.response_average line 65
15. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.mass_pos line 68
16. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.mass_le_one line 72
17. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.mass_sum line 76
18. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.post_prob line 83