OAI/Probability/GaussianInformation/Kernel/NoiseContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Noise.noise_norm_le line 18
2. lemma OAI.KernelPotential.Noise.tendsto_noise_average line 25
3. def OAI.KernelPotential.NoisyDrift.PositiveRule.exactResponse line 57
4. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.measurable_exactResponse line 59
5. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.exactResponse_bounds line 65
6. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.tendsto_response line 78