OAI/Probability/GaussianInformation/Kernel/LocalRules.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KernelPotential.NoisyDrift.LocalRule line 17
2. lemma OAI.KernelPotential.NoisyDrift.LocalRule.le_one line 24
3. def OAI.KernelPotential.NoisyDrift.LocalRule.response line 27
4. lemma OAI.KernelPotential.NoisyDrift.LocalRule.integrable_eval line 29
5. lemma OAI.KernelPotential.NoisyDrift.LocalRule.measurable_response line 38
6. lemma OAI.KernelPotential.NoisyDrift.LocalRule.response_bounds line 43
7. lemma OAI.KernelPotential.NoisyDrift.LocalRule.response_sum line 47
8. def OAI.KernelPotential.NoisyDrift.LocalRule.positive line 52
9. lemma OAI.KernelPotential.NoisyDrift.LocalRule.positive_response line 67