OAI/Probability/GaussianInformation/Kernel/NoisySums.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.NoisyDrift.response_entropy_bound line 17
2. lemma OAI.KernelPotential.NoisyDrift.cutoff_mass_bound line 31
3. lemma OAI.KernelPotential.NoisyDrift.joint_postCharge_bound line 60
4. lemma OAI.KernelPotential.NoisyDrift.positive_noisy_bound line 81